Store M bounds per discrete state.

src/reachability.ml

@@ -91,8 +91,7 @@ struct
   type arg_t = TA.timed_automaton * TA.discrete_state
 
   let inclusion (ta, loc) z1 z2 =
-    let bounds = TA.global_m_bounds ta in
-    let mbounds = Udbml.Carray.to_c bounds (Array.length bounds) in
+    let mbounds = TA.m_bounds ta loc in
     Udbml_priced.PDbm.square_inclusion_exp z1 z2 mbounds
 end
 

src/timedAutomaton.ml

@@ -28,6 +28,7 @@ sig
   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 -> Udbml.Carray.t * Udbml.Carray.t
+  val m_bounds : timed_automaton -> discrete_state -> Udbml.Carray.t
   val global_m_bounds : timed_automaton -> int array
   val global_m_invariant : timed_automaton -> UDbm.Dbm.t
   (** print functions *)
@@ -283,6 +284,7 @@ struct
     query : query;
     lubounds_tbl : (int array * int array) DSHashtbl.t;
     lubounds_tbl_c : (Udbml.Carray.t * Udbml.Carray.t) DSHashtbl.t;
+    mbounds_tbl_c : Udbml.Carray.t DSHashtbl.t;
     guards_tbl : UDbm.Dbm.t GuardHashtbl.t;
     invars_tbl : UDbm.Dbm.t DSHashtbl.t;
     global_mbounds : int array;
@@ -717,6 +719,20 @@ struct
       DSHashtbl.add ta.lubounds_tbl_c state (lar,uar);
       (lar,uar)
 
+  let m_bounds ta state =
+    try
+      DSHashtbl.find ta.mbounds_tbl_c state
+    with Not_found ->
+      let nclocks = VarContext.size ta.clocks in
+      let lower,upper = DSHashtbl.find ta.lubounds_tbl state in
+      let mbound = Array.make nclocks 0 in
+      for cl = 0 to nclocks-1 do
+        mbound.(cl) <- max lower.(cl) upper.(cl)
+      done;
+      let res = Udbml.Carray.to_c mbound nclocks in
+      DSHashtbl.add ta.mbounds_tbl_c state res;
+      res
+
   let global_m_bounds ta =
     if (ta.global_mbounds.(0) <> 0) then (
       let nclocks = VarContext.size (clocks ta) in
@@ -885,7 +901,12 @@ struct
               Stack.push (succ, succ_edges) trace
             end
         end
-    done
+    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
 
   (** Constructs a timed_automaton from the C data structure produced by the
    *  library utap.
@@ -945,6 +966,7 @@ struct
       query = query;
       lubounds_tbl = DSHashtbl.create 1024;
       lubounds_tbl_c = DSHashtbl.create 1024;
+      mbounds_tbl_c = DSHashtbl.create 1024;
       guards_tbl = GuardHashtbl.create 1024;
       invars_tbl = DSHashtbl.create 1024;
       global_mbounds = Array.make (VarContext.size clocks) (-Dbm.infty)