Compute M bounds for clocks.

src/timedAutomaton.ml

@@ -26,6 +26,8 @@ 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 -> int array -> int array -> unit
+  val global_m_bounds : timed_automaton -> int array
+  val global_m_invariant : timed_automaton -> UDbm.Dbm.t
   (** print functions *)
   val print_discrete_state  : 'b BatIO.output -> timed_automaton -> discrete_state -> unit
   val print_transition : 'b BatIO.output -> timed_automaton -> transition -> unit
@@ -581,6 +583,31 @@ struct
       done;
     done
 
+  let global_m_bounds ta =
+    let nclocks = VarContext.size (clocks ta) in
+    let result = Array.make nclocks (-Dbm.infty) in
+    result.(0) <- 0;
+    for cl = 0 to nclocks-1 do
+      for i = 0 to (Array.length ta.lowerLU) - 1 do
+        for j = 0 to (Array.length ta.lowerLU.(i)) - 1 do
+          let mymax (x:int) (y:int) =
+            if (x < y) then y else x
+          in
+          result.(i) <- mymax result.(cl) ta.lowerLU.(i).(j).(cl);
+          result.(i) <- mymax result.(cl) ta.upperLU.(i).(j).(cl)
+        done
+      done;
+    done;
+    result
+
+  let global_m_invariant ta =
+    let marray = global_m_bounds ta in
+    let inv_guard = ref [] in
+    for i = 0 to (Array.length marray)-1 do
+      inv_guard := (GuardLeq (Clock i, Constant marray.(i))) :: !inv_guard
+    done;
+    _guard_to_dbm ta ta.init.stateVars !inv_guard
+    
   (** print functions *)
   let print_discrete_state chan ta state =
     fprintf chan "%s\n" (string_of_state ta state)