Time elapse with a rate

src/costs.ml

@@ -8,6 +8,8 @@ IFDEF ENABLE_CORA THEN
   let edge_cost_def = Constant(0)
   let loc_rate_def = None
 
+  let rate x = x
+
 ELSE
 
   type edge_cost = unit
@@ -16,5 +18,7 @@ ELSE
   let edge_cost_def = ()
   let loc_rate_def = ()
 
+  let rate _ = 1
+
 END
 

src/dbm.ml

@@ -19,7 +19,7 @@ sig
   val to_fed : t -> fed_t
 
   val constrain : t -> Udbml.Basic_types.clock_constraint_t -> unit
-  val up : t -> fed_t
+  val up : t -> int -> fed_t
   val update_value : t -> Udbml.Basic_types.cindex_t -> Udbml.Basic_types.bound_t -> fed_t
   val intersect : t -> Udbml_unpriced.Dbm.t -> unit
 
@@ -41,7 +41,7 @@ sig
   val to_dbm : t -> dbm_t list
   val iter : t -> (dbm_t -> unit) -> unit
 
-  val up : t -> unit
+  val up : t -> int -> unit
   val update_value : t -> Udbml.Basic_types.cindex_t -> Udbml.Basic_types.bound_t -> unit
   val intersect : t -> Udbml_unpriced.Dbm.t -> unit
 end
@@ -72,9 +72,9 @@ struct
 
       let to_fed z = Fed.from_dbm z
 
-      let up z =
+      let up z r =
         let f = to_fed z in
-        Fed.up f;
+        Fed.up f r;
         f
 
       let update_value z c b =
@@ -86,6 +86,8 @@ struct
     struct
       include Udbml_unpriced.Fed
 
+      let up z _ = Udbml_unpriced.Fed.up z
+
       let to_dbm t =
         let res = ref [] in
         iter t (fun z -> res := z :: !res);
@@ -109,9 +111,9 @@ struct
       
       let to_fed z = Fed.from_dbm z
 
-      let up z =
+      let up z r =
         let f = to_fed z in
-        Fed.up f;
+        Fed.up f r;
         f
       
       let update_value z c b =

src/reachability.ml

@@ -278,7 +278,9 @@ struct
       succs_list
     else (
       List.iter (fun (c, v) -> Fed.update_value result_zone c v) resets;
-      if (not (TA.is_urgent_or_committed ta target)) then (Fed.up result_zone);
+      if (not (TA.is_urgent_or_committed ta target)) then (
+        Fed.up result_zone (Costs.rate (TA.rate_of_state ta target));
+      );
       Fed.intersect result_zone (TA.invariant_of_discrete_state ta target);
       (match global_invariant with
       | None -> ()
@@ -335,7 +337,7 @@ struct
     let wot = WO.create () in
     let (init, zinit) = TA.initial_extended_state ta in
     let initfed = Fed.from_dbm zinit in
-    Fed.up initfed;
+    Fed.up initfed (Costs.rate (TA.rate_of_state ta init));
     Fed.intersect initfed (TA.invariant_of_discrete_state ta init);
     List.iter (fun z ->
         ABS.extrapolate z (ta, init);

src/timedAutomaton.ml

@@ -27,6 +27,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 rate_of_state : timed_automaton -> discrete_state -> int
   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
@@ -627,6 +628,11 @@ struct
       inv
        | _ as e -> raise e
 
+  let rate_of_state ta state =
+    Array.fold_left (fun c -> fun loc -> match loc.locRate with
+      | None -> c
+      | Some(e) -> c + eval_disc_exp ta state.stateVars e) 0 state.stateLocs
+
   let initial_extended_state ta =
     let dim = (VarContext.size (clocks ta)) in
     let z = Dbm.create dim in