Commit 8fa2a765 authored by mcolange's avatar mcolange

Improve caching of LU bounds.

parent 7393cefe
......@@ -3,40 +3,6 @@ open Common
open TimedAutomaton
open Uta
module LUCache (TA : TIMED_AUTOMATON) =
struct
module TA_ds =
struct
type t = TA.discrete_state
let hash s = TA.hash_discrete_state s
let equal = TA.is_state_equal
end
module DSHashtbl = Hashtbl.Make(TA_ds)
let lu_memo = DSHashtbl.create 100
let lu_bounds ta loc =
try DSHashtbl.find lu_memo loc
with Not_found -> (
let dim = VarContext.size (TA.clocks ta) in
let (larrtmp, uarrtmp) =
(Array.make dim 0,
Array.make dim 0)
in
TA.lu_bounds ta loc larrtmp uarrtmp;
let (larr, uarr) =
(Udbml.Carray.to_c larrtmp dim, Udbml.Carray.to_c uarrtmp dim)
in
DSHashtbl.add lu_memo loc (larr, uarr);
(larr, uarr)
)
end
(** An abstract type for zone abstractions *)
module type ABSTRACTION =
sig
......@@ -66,10 +32,8 @@ module Extra_LU (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_unpriced.Dbm.
struct
type arg_t = TA.timed_automaton * TA.discrete_state
module LUC = LUCache(TA)
let extrapolate zone (ta, loc) =
let (lbounds, ubounds) = LUC.lu_bounds ta loc in
let (lbounds, ubounds) = TA.lu_bounds ta loc in
Udbml_unpriced.Dbm.extrapolate_lu_bounds zone lbounds ubounds
end
......@@ -112,10 +76,8 @@ module Sri (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_unpriced.Dbm.t) :
struct
type arg_t = TA.timed_automaton * TA.discrete_state
module LUC = LUCache(TA)
let inclusion (ta, loc) z1 z2 =
let (lbounds, ubounds) = LUC.lu_bounds ta loc in
let (lbounds, ubounds) = TA.lu_bounds ta loc in
Udbml_unpriced.Dbm.closure_leq lbounds ubounds z1 z2
end
......
......@@ -25,7 +25,7 @@ sig
val invariant_of_discrete_state : timed_automaton -> discrete_state -> UDbm.Dbm.t
val is_urgent_or_committed : timed_automaton -> discrete_state -> bool
val is_target : timed_automaton -> discrete_state -> bool
val lu_bounds : timed_automaton -> discrete_state -> int array -> int array -> unit
val lu_bounds : timed_automaton -> discrete_state -> Udbml.Carray.t * Udbml.Carray.t
val global_m_bounds : timed_automaton -> int array
val global_m_invariant : timed_automaton -> UDbm.Dbm.t
(** print functions *)
......@@ -118,21 +118,13 @@ struct
struct
type t = location array
exception NotEqual
let equal a1 a2 =
let dim = Array.length a1 in
assert(dim = (Array.length a2));
try
for x = 0 to dim-1 do
if (a1.(x).locId <> a2.(x).locId) then
raise NotEqual
done;
true
with NotEqual -> false
not (Array.exists2 (fun l1 l2 -> not (l1.locId = l2.locId)) a1 a2)
let hash a =
Hashtbl.hash (Array.map (fun x -> x.locId) a)
Array.fold_right
(fun x r -> r + x.locId + 0x9e3779b9 + (r lsl 6) + (r lsr 2))
a 0
end
)
......@@ -151,6 +143,7 @@ struct
mutable upperLU : int array array array;
guards_tbl : (_succinct_transition,UDbm.Dbm.t) Hashtbl.t;
invars_tbl : UDbm.Dbm.t LocHashtbl.t;
lubounds_tbl : (Udbml.Carray.t * Udbml.Carray.t) LocHashtbl.t;
}
......@@ -568,25 +561,29 @@ struct
EmptyQuery -> true
| ReachQuery(pq) -> eval pq
let lu_bounds ta state lbounds ubounds =
Array.iteri (fun i _ ->
lbounds.(i) <- -Dbm.infty;
ubounds.(i) <- -Dbm.infty
) lbounds;
lbounds.(0) <- 0;
ubounds.(0) <- 0;
let nprocs = Array.length state.stateLocs in
let nclocks = VarContext.size ta.clocks in
for iproc = 0 to nprocs - 1 do
let iloc = state.stateLocs.(iproc).locId in
for cl = 0 to nclocks - 1 do
let mymax (x:int) (y:int) =
if (x < y) then y else x
in
lbounds.(cl) <- mymax lbounds.(cl) ta.lowerLU.(iproc).(iloc).(cl);
ubounds.(cl) <- mymax ubounds.(cl) ta.upperLU.(iproc).(iloc).(cl);
let lu_bounds ta state =
try
LocHashtbl.find ta.lubounds_tbl state.stateLocs
with Not_found ->
let mymax (x:int) (y:int) =
if (x < y) then y else x
in
let nclocks = VarContext.size ta.clocks in
let lbounds = Array.make nclocks (-Dbm.infty) in
let ubounds = Array.make nclocks (-Dbm.infty) in
lbounds.(0) <- 0;
ubounds.(0) <- 0;
let nprocs = Array.length state.stateLocs in
for iproc = 0 to nprocs - 1 do
let iloc = state.stateLocs.(iproc).locId in
for cl = 0 to nclocks - 1 do
lbounds.(cl) <- mymax lbounds.(cl) ta.lowerLU.(iproc).(iloc).(cl);
ubounds.(cl) <- mymax ubounds.(cl) ta.upperLU.(iproc).(iloc).(cl);
done;
done;
done
let (lar, uar) = (Udbml.Carray.to_c lbounds nclocks, Udbml.Carray.to_c ubounds nclocks) in
LocHashtbl.add ta.lubounds_tbl state.stateLocs (lar, uar);
(lar, uar)
let global_m_bounds ta =
let nclocks = VarContext.size (clocks ta) in
......@@ -1065,7 +1062,8 @@ struct
lowerLU = [||];
upperLU = [||];
guards_tbl = Hashtbl.create 1024;
invars_tbl = LocHashtbl.create 1024
invars_tbl = LocHashtbl.create 1024;
lubounds_tbl = LocHashtbl.create 1024
}
in
let (lower,upper) = _make_lu_table ta in
......
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