Commit f2fc927c authored by mcolange's avatar mcolange

Cache the results of the translation guard to dbm.

parent 7263cc5a
......@@ -129,9 +129,21 @@ struct
end
)
(** A succinct version of the above to be used in hash tables; we just don't need the variable valuations *)
type _succinct_transition = Suc_InternalTrans of edge
| Suc_SyncTrans of edge * edge
(** A succinct version of the above to be used in hash tables *)
type _succinct_transition = int array * guard
module GuardHashtbl = Hashtbl.Make(
struct
type t = _succinct_transition
let equal x y = x = y
let hash (a,b) =
Array.fold_right
(fun x r -> r + x + 0x9e3779b9 + (r lsl 6) + (r lsr 2))
a (Hashtbl.hash b)
end
)
type timed_automaton = {
procs : process array;
......@@ -141,7 +153,7 @@ struct
mutable query : query;
mutable lowerLU : int array array array;
mutable upperLU : int array array array;
guards_tbl : (_succinct_transition,UDbm.Dbm.t) Hashtbl.t;
guards_tbl : UDbm.Dbm.t GuardHashtbl.t;
invars_tbl : UDbm.Dbm.t LocHashtbl.t;
lubounds_tbl : (Udbml.Carray.t * Udbml.Carray.t) LocHashtbl.t;
}
......@@ -506,45 +518,34 @@ struct
) rchan;
Queue.fold (fun l tr -> tr :: l) [] transq
let transition_fields ta = function
let guard_of_transition ta tr =
let to_succinct = function
|InternalTrans(s,e) -> (s.stateVars,e.edgeGuard)
|SyncTrans(s,e1,e2) -> (s.stateVars,List.rev_append e1.edgeGuard e2.edgeGuard)
in
let (vars,succ_guard) as str = to_succinct tr in
try
GuardHashtbl.find ta.guards_tbl str
with Not_found ->
let g = _guard_to_dbm ta vars succ_guard in
GuardHashtbl.add ta.guards_tbl str g;
g
| _ as e -> raise e
let transition_fields ta tr = match tr with
| InternalTrans(state, e) ->
let state' = _copy_state state in
_apply_edge ta state e state';
(state,
_guard_to_dbm ta state.stateVars e.edgeGuard,
guard_of_transition ta tr,
e.edgeReset,
state')
| SyncTrans(state, e1, e2) ->
let state' = _copy_state state in
_apply_edge ta state e1 state';
_apply_edge ta state e2 state';
let g1 = _guard_to_dbm ta state.stateVars e1.edgeGuard in
let g2 = _guard_to_dbm ta state.stateVars e2.edgeGuard in
UDbm.Dbm.intersect g1 g2;
(state, g1, (ClockSet.union e1.edgeReset e2.edgeReset), state')
let guard_of_transition ta tr =
let to_succinct = function
|InternalTrans(_,e) -> Suc_InternalTrans(e)
|SyncTrans(_,e1,e2) -> Suc_SyncTrans(e1,e2)
in
let str = to_succinct tr in
try
Hashtbl.find ta.guards_tbl str
with Not_found ->
(match tr with
| InternalTrans(state,e) ->
let g =_guard_to_dbm ta state.stateVars e.edgeGuard in
Hashtbl.add ta.guards_tbl str g;
g
| SyncTrans(state,e1,e2) ->
let g1 = _guard_to_dbm ta state.stateVars e1.edgeGuard in
let g2 = _guard_to_dbm ta state.stateVars e2.edgeGuard in
UDbm.Dbm.intersect g1 g2;
Hashtbl.add ta.guards_tbl str g1;
g1
)
|_ as e -> raise e
let g = guard_of_transition ta tr in
(state, g, (ClockSet.union e1.edgeReset e2.edgeReset), state')
let is_urgent_or_committed ta state =
Array.exists (fun loc -> loc.locCommitted || loc.locUrgent) state.stateLocs
......@@ -1061,7 +1062,7 @@ struct
query = EmptyQuery;
lowerLU = [||];
upperLU = [||];
guards_tbl = Hashtbl.create 1024;
guards_tbl = GuardHashtbl.create 1024;
invars_tbl = LocHashtbl.create 1024;
lubounds_tbl = LocHashtbl.create 1024
}
......
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