From a0eda0df651cf1793389e3c2a583575ad5c99eaa Mon Sep 17 00:00:00 2001
From: Maximilien Colange
Date: Wed, 6 Apr 2016 01:04:08 +0200
Subject: [PATCH] Optimize LU bounds computation.

src/uppaalta.ml  62 ++++++++++++++
1 file changed, 17 insertions(+), 45 deletions()
diff git a/src/uppaalta.ml b/src/uppaalta.ml
index b21cf9b..1b687f7 100644
 a/src/uppaalta.ml
+++ b/src/uppaalta.ml
@@ 607,24 +607,6 @@ struct
(********** LOADING FUNCTIONS **********)
 (** given a set of expressions, simplify it to retain only its maximal
 * constant and all nonconstant *)
 (* TODO check that the input does not contain ConstVariable or constant ConstArray *)
 let simplify_max exprs =
 let new_max = function
  None > (function
  Constant k > Some k
  _ > None)
  Some m as e > (function
  Constant k when k > m > Some k
  _ > e)
 in
 match List.fold_left new_max None exprs with
  None > exprs
  Some k > List.filter (function
  Constant l when l < k > false
  _ > true) exprs

(* given a process, a location l and a clock c, compute the set of expressions
* against which c is compared from l until it is reset.
* Formally, the result S is the smallest set of expressions such that:
@@ 645,39 +627,29 @@ struct
let n = VarContext.size ta.clocks in
let lb, ub = Array.make n 0, Array.make n 0 in
let eval = eval_exp ta state.stateVars in
 for cl=0 to n1 do
 let lexpr, uexpr = Array.fold_left
 (fun (lacc, uacc) loc >
+ for cl=1 to n1 do
+ Array.iter
+ (fun loc >
let ltmp, utmp = loc.compExpr.(cl) in
 (lacc @ ltmp, uacc @ utmp)) ([],[])
+ (* instantiate found expressions, and retain only the maximal constant *)
+ List.iter (fun e >
+ match eval e with
+  Constant k when k > lb.(cl) > lb.(cl) < k
+  Constant _ > ()
+  _ > failwith "expression does not evaluate to constant")
+ ltmp;
+ List.iter (fun e >
+ match eval e with
+  Constant k when k > ub.(cl) > ub.(cl) < k
+  Constant _ > ()
+  _ > failwith "expression does not evaluate to constant")
+ utmp)
state.stateLocs
 in
 (* instantiate found expressions, and retain only the maximal constant *)
 let lcst, ucst =
 simplify_max (List.map eval lexpr),
 simplify_max (List.map eval uexpr)
 in
 begin
 match lcst with
  (Constant k)::_ > lb.(cl) < max lb.(cl) k
  _ > (* TODO can it happen? *) ()
 end;
 begin
 match ucst with
  (Constant k)::_ > ub.(cl) < max ub.(cl) k
  _ > (* TODO can it happen? *) ()
 end;
done;
lb, ub
let lubounds ta state =
 try
 DSHashtbl.find ta.lubounds_tbl state
 with
  Not_found >
 let res = _lubounds ta state in
 DSHashtbl.add ta.lubounds_tbl state res;
 res
+ _lubounds ta state
(* tells whether a given clock is set by a given update *)
(* the difficult part is when the lhs of the update is an array cell *)

2.24.1