Commit de9b6905 authored by Benoit Barbot's avatar Benoit Barbot
Browse files

try lu extrapolation

parent 113b5289
Pipeline #2988 passed with stages
in 25 seconds
......@@ -289,10 +289,10 @@ module ExactReachability (Model : TimedAutomaton.TIMED_AUTOMATON) = struct
a
in
let dim = Uppaal_parser.Uta.VarContext.size (Model.clocks ta) + 1 in
let int_lbounds = Array.make dim 0 in
let int_ubounds = Array.make dim 0 in
(*let int_max_bound = Model.max_bound ta in*)
(*let dim = Uppaal_parser.Uta.VarContext.size (Model.clocks ta) + 1 in
let int_lbounds = Array.make dim 0 in
let int_ubounds = Array.make dim 0 in*)
let int_max_bound = Model.max_bound ta in
let stmap = LocZoneHashtbl.create 100 in
let to_visit_list = Queue.create () in
let linit, zinit = Model.initial_extended_state ta in
......@@ -328,11 +328,12 @@ module ExactReachability (Model : TimedAutomaton.TIMED_AUTOMATON) = struct
(* z is the entry zone in post state; g2 is the guard intersected with TE(entryzone) and invariant *)
try
let g2, z =
post ta
~extrapolate:(fun z ->
post
ta
(*~extrapolate:(fun z ->
Model.lu_bounds ta st.disc_state int_lbounds int_ubounds;
Dbm.extrapolate_lu z int_lbounds int_ubounds)
(*~extrapolate:(fun z -> Dbm.cClosure z int_max_bound)*)
Dbm.extrapolate_lu z int_lbounds int_ubounds)*)
~extrapolate:(fun z -> Dbm.cClosure z int_max_bound)
st e
in
......
Supports Markdown
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