Commit a0eda0df authored by Maximilien Colange's avatar Maximilien Colange

Optimize LU bounds computation.

parent 832da45c
......@@ -607,24 +607,6 @@ struct
(********** LOADING FUNCTIONS **********)
(** given a set of expressions, simplify it to retain only its maximal
* constant and all non-constant *)
(* 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 n-1 do
let lexpr, uexpr = Array.fold_left
(fun (lacc, uacc) loc ->
for cl=1 to n-1 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 *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment