Pass a Dbm module to Timed Automata.

Preparatory work for priced zones.

src/main.ml

@@ -64,7 +64,7 @@ let execute tafile qfile =
   let module WO = WO_tmp(Uta_ds) in
   let module Abs = (val !Options.abstraction : UTA_ABSTRACTION) in
   let module Incl = (val !Options.inclusion : UTA_INCLUSION) in
-  let module Reach = Reachability(Uautomaton)(WO)(Abs)(Incl) in
+  let module Reach = Reachability(Uautomaton)(WO(Uautomaton.Dbm))(Abs)(Incl) in
   match (Reach.reach ta) with
   | true -> Log.info "reachable!\n"
   | false -> Log.info "not reachable...\n"

src/options.ml

 open Reachability
 open TimedAutomaton
+open Udbml
 
 type ta_discrete = Uautomaton.timed_automaton * Uautomaton.discrete_state
-module type UTA_ABSTRACTION = ABSTRACTION with type arg_t = ta_discrete
-module type UTA_INCLUSION = INCLUSION with type arg_t = ta_discrete
+module type UTA_ABSTRACTION =
+  ABSTRACTION with type arg_t = ta_discrete
+              and type dbm_t := Uautomaton.Dbm.t
+
+module type UTA_INCLUSION =
+  INCLUSION with type arg_t = ta_discrete
+            and type dbm_t := Uautomaton.Dbm.t
+
 module type UTA_WALK_ORDER =
   functor (Key : Hashtbl.HashedType with type t = Uautomaton.discrete_state) ->
-    WALK_ORDER with type key = Uautomaton.discrete_state
+    functor (Dbm : GEN_IDBM) ->
+      WALK_ORDER  with type key = Uautomaton.discrete_state
+                  and type dbm_t := Dbm.t
 
 module Uta_ds : Hashtbl.HashedType with type t = Uautomaton.discrete_state =
 struct

src/reachability.ml

 open Batteries
 open Common
 open TimedAutomaton
-open Udbml
 open Uta
 
 module LUCache (TA : TIMED_AUTOMATON) = 
@@ -43,14 +42,16 @@ module type ABSTRACTION =
 sig
   (* the abstract type for a possible additional argument *)
   type arg_t
+  type dbm_t
 
-  val extrapolate : Dbm.t -> arg_t -> unit
+  val extrapolate : dbm_t -> arg_t -> unit
 end
 
 (** ID abstraction
  *)
 module ID_abstraction (TA : TIMED_AUTOMATON) :
-  ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state =
+  ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state
+              and type dbm_t := TA.Dbm.t =
 struct
   type arg_t = TA.timed_automaton * TA.discrete_state
 
@@ -60,7 +61,8 @@ end
 (** LU abstraction
  *)
 module Extra_LU (TA : TIMED_AUTOMATON) :
-  ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state =
+  ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state
+              and type dbm_t := TA.Dbm.t =
 struct
   type arg_t = TA.timed_automaton * TA.discrete_state
 
@@ -68,7 +70,7 @@ struct
 
   let extrapolate zone (ta, loc) =
     let (lbounds, ubounds) = LUC.lu_bounds ta loc in
-    Dbm.extrapolate_lu_bounds zone lbounds ubounds
+    TA.Dbm.extrapolate_lu_bounds zone lbounds ubounds
 
 end
 
@@ -81,17 +83,19 @@ module type INCLUSION =
 sig
   (* the abstract type for a possible additional argument *)
   type arg_t
+  type dbm_t
 
-  val inclusion : arg_t -> Dbm.t -> Dbm.t -> bool
+  val inclusion : arg_t -> dbm_t -> dbm_t -> bool
 end
 
 (** Vanilla inclusion *)
 module Inclusion (TA : TIMED_AUTOMATON) :
-  INCLUSION with type arg_t = TA.timed_automaton * TA.discrete_state =
+  INCLUSION with type arg_t = TA.timed_automaton * TA.discrete_state
+            and type dbm_t := TA.Dbm.t =
 struct
   type arg_t = TA.timed_automaton * TA.discrete_state
 
-  let inclusion _ = Dbm.leq
+  let inclusion _ = TA.Dbm.leq
 end
 
 (** Smart inclusion test, based on (insert reference here)
@@ -103,7 +107,8 @@ end
  *                            and   Z'_{x,y} + (<, - L_y) < Z_{x,0}
  *)
 module Sri (TA : TIMED_AUTOMATON) :
-  INCLUSION with type arg_t = TA.timed_automaton * TA.discrete_state =
+  INCLUSION with type arg_t = TA.timed_automaton * TA.discrete_state
+            and type dbm_t := TA.Dbm.t =
 struct
   type arg_t = TA.timed_automaton * TA.discrete_state
 
@@ -111,23 +116,27 @@ struct
 
   let inclusion (ta, loc) z1 z2 =
     let (lbounds, ubounds) = LUC.lu_bounds ta loc in
-    Dbm.closure_leq lbounds ubounds z1 z2
+    TA.Dbm.closure_leq lbounds ubounds z1 z2
 end
 
 (** An abstract type for the walk order of a graph *)
 (** TODO  Operations returning unit are very imperative style...
  *        but efficiency should prevail
+ *  TODO  Make a functor that takes a TA and returns a
+ *        WALK_ORDER with type dbm_t := TA.Dbm.t
  *)
 module type WALK_ORDER =
 sig
   type key
   type t
 
+  type dbm_t
+
   val create : unit -> t
-  val mark : (key -> Dbm.t -> Dbm.t -> bool) -> t -> key * Dbm.t -> unit
-  val is_marked : (key -> Dbm.t -> Dbm.t -> bool) -> t -> key * Dbm.t -> bool
-  val add : t -> key * Dbm.t -> unit
-  val get_next : t -> key * Dbm.t
+  val mark : (key -> dbm_t -> dbm_t -> bool) -> t -> key * dbm_t -> unit
+  val is_marked : (key -> dbm_t -> dbm_t -> bool) -> t -> key * dbm_t -> bool
+  val add : t -> key * dbm_t -> unit
+  val get_next : t -> key * dbm_t
   val finished : t -> bool
 end
 
@@ -147,8 +156,10 @@ end
 
 (** Builds an effective walk order, given a WAIT_CONTAINER and an INCLUSION.
  *)
-module Walk_Order (Cont : WAIT_CONTAINER) (Key : Hashtbl.HashedType)
-  : WALK_ORDER with type key = Key.t =
+module Walk_Order (Cont : WAIT_CONTAINER)
+                  (Key : Hashtbl.HashedType)
+                  (Dbm : GEN_IDBM)
+  : WALK_ORDER with type key = Key.t and type dbm_t := Dbm.t =
 struct
 
   module KeyHashtbl = Hashtbl.Make(Key)
@@ -206,12 +217,18 @@ module Walk_BFS = Walk_Order (Queue)
  *  and will thus be functors of TIMED_AUTOMATON *)
 module TA_RG_WALK =
   functor (TA : TIMED_AUTOMATON) ->
-    functor (WO : WALK_ORDER with type key = TA.discrete_state) ->
+    functor (WO : WALK_ORDER  with type key = TA.discrete_state
+                              and type dbm_t := TA.Dbm.t) ->
       functor (ABS : ABSTRACTION
-          with type arg_t = TA.timed_automaton * TA.discrete_state) ->
+          with type arg_t = TA.timed_automaton * TA.discrete_state
+          and type dbm_t := TA.Dbm.t) ->
         functor (COMP : INCLUSION
-            with type arg_t = TA.timed_automaton * TA.discrete_state) ->
+            with type arg_t = TA.timed_automaton * TA.discrete_state
+            and type dbm_t := TA.Dbm.t) ->
 struct
+
+  module Dbm = TA.Dbm
+
   (** Auxiliary function that computes the list of successors of an
    *  extended state.
    *  Not intended to be called from the outside.
@@ -295,11 +312,14 @@ end
 
 module Reachability =
   functor (TA : TIMED_AUTOMATON) ->
-    functor (WO : WALK_ORDER with type key = TA.discrete_state) ->
+    functor (WO : WALK_ORDER with type key = TA.discrete_state
+                              and type dbm_t := TA.Dbm.t) ->
       functor (ABS : ABSTRACTION
-          with type arg_t = TA.timed_automaton * TA.discrete_state) ->
+          with type arg_t = TA.timed_automaton * TA.discrete_state
+          and type dbm_t := TA.Dbm.t) ->
         functor (COMP : INCLUSION
-            with type arg_t = TA.timed_automaton * TA.discrete_state) ->
+            with type arg_t = TA.timed_automaton * TA.discrete_state
+            and type dbm_t := TA.Dbm.t) ->
 struct
   module Walker = TA_RG_WALK(TA)(WO)(ABS)(COMP)
 

src/timedAutomaton.ml

@@ -4,8 +4,12 @@ open Printf
 open Udbml
 open Uta
 
+module type GEN_IDBM = Udbml.IDBM with type cindex_t = int and type bound_t = int
+
 module type TIMED_AUTOMATON =
 sig
+  module Dbm : GEN_IDBM
+
   type timed_automaton
   type discrete_state
   type transition
@@ -39,9 +43,11 @@ sig
   val is_controllable : timed_automaton -> edge -> bool
 end
 
-(** TODO allow to pass a DBM type? *)
-module GenericUAutomaton =
+module GenericUAutomaton (Dbm : GEN_IDBM) =
 struct
+
+  module Dbm = Dbm
+
   (** In contrast with Uta.expression used in the parser, the variables here are indexed
    *  by unique integer identifiers.
    *)
@@ -1077,5 +1083,5 @@ struct
   
 end
 
-module Uautomaton = GenericUAutomaton
+module Uautomaton = GenericUAutomaton(Dbm)