Skip to content

T
tiamo
Commit 7e66225e authored by Maximilien Colange's avatar Maximilien Colange
Browse files
Options

Merge branch 'master' into tests

parents e31af3d8 5c1cb14e
Hide whitespace changes
Inline Side-by-side
Showing with 209 additions and 152 deletions
src/options.ml
View file @ 7e66225e
......@@ -143,11 +143,6 @@ struct
Arg.Unit (function () -> Costs.enable_cora := true),
" Enable CORA-syntax support for priced models (not activated by default)");
( "-mbounded",
Arg.Unit (function () -> do_bound := true),
" Use the (global M)-bounded version of the input automaton.
\tThis induces a performance hit, but guarantees termination of algorithms when you are not sure whether the input automaton is bounded or not.");
( "-order",
Arg.String (function
| "BFS" -> walk_order := (module Waiting.Walk_BFS : PARTIAL_WO)
......
src/uppaalta.ml
View file @ 7e66225e
......@@ -112,7 +112,9 @@ struct
}
and location = {
locId : int;
(* the ID of the location *)
mutable locName : string;
(* the name of the location, for printing purposes *)
locCommitted : bool;
locUrgent : bool;
locInvar : guard;
......@@ -121,6 +123,12 @@ struct
locRate : Costs.loc_rate;
(* the cost rate of time elapsing in this location [default is None] *)
(* the cost rate of an array of location is the sum of their cost rates *)
mutable compExpr : ((expression list) * (expression list)) array;
(* compExpr.(cl) contains the set of expressions against which cl is
* compared in any guard or invariant from the current location until
* it is reset. First component for L bounds, second one for U bounds.
* Local computation of LU bounds, useful for the global computation.
*)
}
and process = {
procName : string;
......@@ -581,23 +589,9 @@ struct
in
eval_query ta.query
let lubounds ta state =
DSHashtbl.find ta.lubounds_tbl state
(* TODO *)
let global_mbounds ta =
if (ta.global_mbounds.(0) <> 0) then (
let nclocks = VarContext.size (clocks ta) in
ta.global_mbounds.(0) <- 0;
DSHashtbl.iter (fun _ -> fun (lbound,ubound) ->
for cl = 0 to nclocks-1 do
ta.global_mbounds.(cl) <- max ta.global_mbounds.(cl) lbound.(cl);
ta.global_mbounds.(cl) <- max ta.global_mbounds.(cl) ubound.(cl)
done) ta.lubounds_tbl;
Array.iteri (fun cl m ->
if (m < 0) then
printf "clock %d (of bound %d) is never read!?\n" cl m) ta.global_mbounds
);
ta.global_mbounds
failwith "not implemented"
(** print functions *)
let print_discrete_state chan ta state =
......@@ -612,140 +606,207 @@ struct
Array.iter (fun proc -> fprintf chan "%s\n-----\n" (string_of_process ta proc)) ta.procs
(********** LOADING FUNCTIONS **********)
(* propagate the clocks given in input, and return a set of clocks still
* worth to propagate
*)
let propagate lparent uparent lson uson updates clocks =
let res = ref ClockSet.empty in
(* for every element of clocks, check whether to propagate *)
ClockSet.iter (fun cl ->
(* a clock does not propagate past an update *)
if (List.for_all (fun (i,_) -> i <> cl) updates) then
begin
(* a clock is worth propagating later on if it propagates here *)
if (lparent.(cl) < lson.(cl)) then (
lparent.(cl) <- lson.(cl);
res := ClockSet.add cl !res
);
if (uparent.(cl) < uson.(cl)) then (
uparent.(cl) <- uson.(cl);
res := ClockSet.add cl !res
)
end) clocks;
!res
exception Early_stop
(** To compute LU (and M) bounds, we first explore the whole discrete
* state space.
* At each discrete state s, each clock c is given the largest constant
* against which it is compared in s.
* Then, larger bounds propagate backwards, but not CROSS resets.
* The best way to do this (with the retropropagation) is a DFS of the
* discrete state space
*)
(* TODO by adapting the walk order, the M bounds could be computed on the fly,
* while the real state space is being discovered
(** 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:
* if x is compared to e in the invariant of l, then e \in S
* for any transition t : l->l'
* if x is compared to e in the guard of t, then e \in S
* if x is not reset in t, then comp_expressions p l' c \subset S
* returns a pair (L,U)
*)
let comp_expressions ta p l c =
ta.procs.(p).procLocations.(l).compExpr.(c)
(* computes the LU bounds in a given state *)
(* this should be used from another function that caches the results *)
(* TODO some clocks already have their constant known, cache them *)
let _lubounds ta state =
let n = nb_clocks ta in
let lb, ub = Array.make n 0, Array.make n 0 in
for cl=0 to n-1 do
let lexpr, uexpr = Array.fold_left
(fun (lacc, uacc) loc ->
let ltmp, utmp = loc.compExpr.(cl) in
(lacc @ ltmp, uacc @ utmp)) ([],[])
state.stateLocs
in
(* instantiate found expressions, and retain only the maximal constant *)
let lcst, ucst =
simplify_max (List.map (fun e -> eval_exp ta state.stateVars e) lexpr),
simplify_max (List.map (fun e -> eval_exp ta state.stateVars e) 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
(* 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 *)
let is_reset : clock_t -> update -> bool = fun cl -> function
| ClockRef c, _ when c = cl -> true
| ClockArrayRef (a,_), _ ->
(* TODO true if cl is a cell of the array a, false otherwise *)
(* TODO further refine: if all indices expressions are constant, we
* can do an exact equality check *)
failwith "cannot compute bounds for arrays of clocks"
| _ -> false
(* return the set of clock the argument can refer to *)
let clocks_of ta = function
| Clock c -> [c]
| ClockArray(a,_) -> (*TODO*) failwith "cannot compute bounds for arrays of clocks"
| _ -> []
(* compute all the local LU bounds *)
let build_lu ta =
let nclocks = VarContext.size ta.clocks in
let trace = Stack.create () in
(* trace is a stack of discrete_state * (transition list) *)
(* to get a list of transitions from a discrete state, use _transitions_from *)
let init = initial_state ta in
let init_edges = _transitions_from ta init in
Stack.push (init, init_edges) trace;
let ltmp, utmp = Array.make nclocks min_int, Array.make nclocks min_int in
DSHashtbl.add ta.lubounds_tbl init (ltmp,utmp);
while (not (Stack.is_empty trace)) do
let (current, edges) = Stack.top trace in
match edges with
| [] -> begin
(* pop the stack *)
let _ = Stack.pop trace in
(* we are done with this state, retropropagation *)
let son = ref current in
let clocks = ref ClockSet.empty in
for cl = 1 to nclocks-1 do clocks := ClockSet.add cl !clocks done;
(* Do the bound retropropagation *)
begin
try
Stack.iter (fun (parent, edge :: _) ->
if (ClockSet.is_empty !clocks) then
raise Early_stop;
let lson,uson = DSHashtbl.find ta.lubounds_tbl !son in
let lparent,uparent = DSHashtbl.find ta.lubounds_tbl parent in
let (_,_,updates,_) = transition_fields ta edge in
clocks := propagate lparent uparent lson uson updates !clocks;
son := parent
) trace;
with
| Early_stop -> ()
end;
(* get the parent state, its first edge is the one between parent and current *)
if (not (Stack.is_empty trace)) then (
let (parent, _::l) = Stack.pop trace in
(* repush the parent and its remaining edges *)
Stack.push (parent, l) trace;
)
end
| edge :: rest -> begin
let (_,guard,updates,succ) = transition_fields ta edge in
let (current_lower,current_upper) = DSHashtbl.find ta.lubounds_tbl current in
(* evaluate accesses to clock arrays, if any *)
(* TODO refactor: the guard should already be evaluated by _transition_fields *)
let evalClock = fun (ClockArray(i,ilist)) ->
let indices = List.map (fun e -> eval_disc_exp ta current.stateVars e) ilist in
let cid = VarContext.index_of_cell ta.clocks i indices in
Clock(cid)
in
let guard_eval = List.map (function
| GuardLeq(ClockArray(_,_) as ca,rhs) -> GuardLeq(evalClock ca,rhs)
| GuardLess(ClockArray(_,_) as ca,rhs) -> GuardLess(evalClock ca,rhs)
| GuardEqual(ClockArray(_,_) as ca,rhs) -> GuardEqual(evalClock ca,rhs)
| GuardGeq(ClockArray(_,_) as ca,rhs) -> GuardGeq(evalClock ca,rhs)
| GuardGreater(ClockArray(_,_) as ca,rhs) -> GuardGeq(evalClock ca,rhs)
| _ as x -> x) guard
in
(* update the bounds of current thanks to current transition *)
List.iter (function
| GuardLeq(Clock(cl),e)
| GuardLess(Clock(cl),e) ->
let r = eval_disc_exp ta current.stateVars e in
current_upper.(cl) <- max current_upper.(cl) r
| GuardEqual(Clock(cl),e) ->
let r = eval_disc_exp ta current.stateVars e in
current_upper.(cl) <- max current_upper.(cl) r;
current_lower.(cl) <- max current_lower.(cl) r
| GuardGeq(Clock(cl),e)
| GuardGreater(Clock(cl),e) ->
let r = eval_disc_exp ta current.stateVars e in
current_lower.(cl) <- max current_lower.(cl) r
| _ -> failwith "cannot compute LU bounds, guard not in normal form")
guard_eval;
(* now take care of the succ *)
if (DSHashtbl.mem ta.lubounds_tbl succ) then
(* if already discovered, push it on the stack with an empty list of
* edges in order to have the correct retropropagation *)
begin
Stack.push (succ, []) trace
end
else
(* if new, add it to the hashtable and push it on the stack *)
begin
let ltmp, utmp = Array.make nclocks min_int, Array.make nclocks min_int in
DSHashtbl.add ta.lubounds_tbl succ (ltmp,utmp);
let succ_edges = _transitions_from ta succ in
Stack.push (succ, succ_edges) trace
end
end
done;
DSHashtbl.iter (fun _ -> fun (lbound,ubound) ->
for cl=0 to nclocks-1 do
if (lbound.(cl) < 0) then lbound.(cl) <- 0;
if (ubound.(cl) < 0) then ubound.(cl) <- 0
done) ta.lubounds_tbl
(* for each process *)
for p=0 to (Array.length ta.procs)-1 do
let proc = ta.procs.(p) in
(* initialization: for each location, add the expression of its invariant
* and of guards of outgoing transitions
*)
for l=0 to (Array.length proc.procLocations)-1 do
let loc = proc.procLocations.(l) in
loc.compExpr <- Array.make nclocks ([],[]);
let ag_handle = function
| GuardLeq(lhs,e)
| GuardLess(lhs,e) ->
List.iter
(fun cl ->
let ltmp, utmp = loc.compExpr.(cl) in
if not (List.mem e utmp) then
loc.compExpr.(cl) <- ltmp, e::utmp
)
(clocks_of ta lhs)
| GuardGeq(lhs,e)
| GuardGreater(lhs,e) ->
List.iter
(fun cl ->
let ltmp, utmp = loc.compExpr.(cl) in
if not (List.mem e ltmp) then
loc.compExpr.(cl) <- e::ltmp, utmp
)
(clocks_of ta lhs)
| GuardEqual(lhs,e) ->
List.iter
(fun cl ->
let ltmp, utmp = loc.compExpr.(cl) in
let lnew =
if not (List.mem e ltmp) then
e::ltmp
else
ltmp
in
let unew =
if not (List.mem e utmp) then
e::utmp
else
utmp
in
loc.compExpr.(cl) <- lnew, unew
)
(clocks_of ta lhs)
| _ -> failwith "cannot compute LU bounds, guard is not in normal form"
in
(* add invariant contribution *)
List.iter ag_handle loc.locInvar;
(* for each transition, add guard contribution *)
List.iter (fun edge ->
List.iter ag_handle edge.edgeGuard)
loc.locEdges
done;
(* fixpoint computation
* for each location l, for each transition t from l to l',
* for each clock c,
* if c is not reset by t, add the expressions for c from l' in l
* if the set for l changes in the operation, remember to loop once more
*)
let stable = ref false in
while not !stable do
stable := true;
(* for each location *)
for l=0 to (Array.length proc.procLocations)-1 do
let loc = proc.procLocations.(l) in
(* iterate over the transitions *)
List.iter (fun edge ->
(* for each clock *)
for cl=0 to nclocks-1 do
(* if it is not reset *)
if List.for_all (fun u -> not (is_reset cl u)) edge.edgeUpdates then
begin
let lcurrent, ucurrent = loc.compExpr.(cl) in
(* update lower bounds *)
let lnew = List.fold_left (fun acc e ->
if not (List.mem e acc) then (
stable := false;
e::acc
) else (
acc
)
) lcurrent (fst proc.procLocations.(edge.edgeTarget).compExpr.(cl))
in
(* update upper bounds *)
let unew = List.fold_left (fun acc e ->
if not (List.mem e acc) then (
stable := false;
e::acc
) else (
acc
)
) ucurrent (snd proc.procLocations.(edge.edgeTarget).compExpr.(cl))
in
(* do the actual update *)
loc.compExpr.(cl) <- lnew, unew
end
done
) loc.locEdges
done
done
done
(** Constructs a timed_automaton from the C data structure produced by the
* library utap.
......@@ -1020,6 +1081,7 @@ struct
locEdges = edges;
locProc = procId;
locRate = costRate;
compExpr = Array.make 0 ([],[]); (* actually built during LU bounds computation *)
}
in
Callback.register "cb_build_location" build_location;
......
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