Merge branch 'dynload'

src/ita.ml

@@ -17,11 +17,11 @@ type guard_t = atomic_guard list
 
 (* a printer for an atomic guard *)
 let print_ag clocks = function
-  | LT(c,k) -> (VarContext.var_of_index clocks c) ^ " < " ^ (string_of_int k)
-  | LEQ(c,k) -> (VarContext.var_of_index clocks c) ^ " <= " ^ (string_of_int k)
-  | GT(c,k) -> (VarContext.var_of_index clocks c) ^ " > " ^ (string_of_int k)
-  | GEQ(c,k) -> (VarContext.var_of_index clocks c) ^ " <= " ^ (string_of_int k)
-  | EQ(c,k) -> (VarContext.var_of_index clocks c) ^ " == " ^ (string_of_int k)
+  | LT(c,k) -> (clocks c) ^ " < " ^ (string_of_int k)
+  | LEQ(c,k) -> (clocks c) ^ " <= " ^ (string_of_int k)
+  | GT(c,k) -> (clocks c) ^ " > " ^ (string_of_int k)
+  | GEQ(c,k) -> (clocks c) ^ " <= " ^ (string_of_int k)
+  | EQ(c,k) -> (clocks c) ^ " == " ^ (string_of_int k)
 
 (* a printer for a guard *)
 let rec print_guard clocks = function
@@ -38,8 +38,8 @@ type reset_t = Common.clock_t * int
 (* a printer for a list of resets *)
 let rec print_resets clocks = function
   | [] -> " "
-  | [(c,k)] -> VarContext.var_of_index clocks c ^ " := " ^ (string_of_int k)
-  | (c,k) :: l -> VarContext.var_of_index clocks c ^ " := " ^ (string_of_int k) ^ (print_resets clocks l)
+  | [(c,k)] -> clocks c ^ " := " ^ (string_of_int k)
+  | (c,k) :: l -> clocks c ^ " := " ^ (string_of_int k) ^ (print_resets clocks l)
 
 (**
  * The interface of Timed Automaton to implement when you want to provide
@@ -50,8 +50,15 @@ sig
   type ta
   type state
 
-  (* retrieves ALL the clocks of the model *)
-  val clocks : ta -> VarContext.t
+  (* the number of clocks *)
+  (**
+   * WARNING: clocks are numbered from 1 to nb_clocks
+   *          the clock of index 0 (reference clock) is implicit.
+   *          DO NOT account for clock 0 in nb_clocks.
+   *)
+  val nb_clocks : ta -> int
+  (* clock names *)
+  val string_of_clock : ta -> int -> string
 
   (* the initial state *)
   val initial_state : ta -> state

src/ita.mli

+(**
+ * an atomic guard is a tuple (c,k,r), where c is a clock id (see VarContext)
+ * and k is a constant and r is one of <, <=, >, >= or ==.
+ * Diagonal guards are not allowed.
+ *)
+type atomic_guard =
+    LT of int * int
+  | LEQ of int * int
+  | GT of int * int
+  | GEQ of int * int
+  | EQ of int * int
+
+(* a guard is a conjunction of atomic guards *)
+type guard_t = atomic_guard list
+
+
+(**
+ * a reset is a pair (c,k), where c is a clock id (see VarContext)
+ * and k is a constant.
+ *)
+type reset_t = Common.clock_t * int
+
+(** Printing functions *)
+(* they are provided to help you pretty-print your custom automaton *)
+(* Those functions need to know the clock names, so the first argument
+ * you must provide is a function that associates a name to a clock index
+ * Typical usage:
+   * let print_timed_automaton channel ta =
+   *    ...print locations and stuff...
+   *    Printf.printf "%s" (print_guard (string_of_clock ta) my_fancy_guard);
+   *    ...print other stuff...
+   *    Printf.printf "%s" (print_resets (string_of_clock ta) my_fancy_resets);
+   *    ...print more stuff...
+ *)
+
+(* a printer for an atomic guard *)
+val print_ag : (int -> string) -> atomic_guard -> string
+(* a printer for a guard *)
+val print_guard : (int -> string) -> guard_t -> string
+(* a printer for a list of resets *)
+val print_resets : (int -> string) -> reset_t list -> string
+
+(**
+ * The interface of Timed Automaton to implement when you want to provide
+ * your model as a compiled OCaml object.
+ *)
+module type TA =
+sig
+  type ta
+  type state
+
+  (* the number of clocks *)
+  (**
+   * WARNING: clocks are numbered from 1 to nb_clocks
+   *          the clock of index 0 (reference clock) is implicit.
+   *          DO NOT account for clock 0 in nb_clocks.
+   *)
+  val nb_clocks : ta -> int
+  (* clock names *)
+  val string_of_clock : ta -> int -> string
+
+  (* the initial state *)
+  val initial_state : ta -> state
+  (* utility functions about states *)
+  val hash_state : state -> int
+  val equal_state : state -> state -> bool
+  (* encodes the query on the model *)
+  val is_target : ta -> state -> bool
+
+  (* priority_compare s1 s2 is true iff s1 should be explored before s2 *)
+  (* this allows the modeller to provide heuristics about the exploration of
+   * the state space *)
+  val priority_compare : state -> state -> int
+
+  (* the transitions out of a state *)
+  val transitions_from : ta -> state -> (state * guard_t * (reset_t list) * state) list
+  (* the invariant of a state *)
+  val invariant : ta -> state -> guard_t
+  (* whether time can elapse in the state *)
+  val is_urgent_or_committed : ta -> state -> bool
+  (* the rate of a state *)
+  val rate_of_state : ta -> state -> int
+  
+  (* the LU bounds (per clock) of a state *)
+  (**
+   * NB:  larger bounds do not impact correctness.
+   *      When in doubt, pick too large bounds.
+   *      Remember that tight bounds yield better performance.
+   *)
+  val lubounds : ta -> state -> int array * int array
+  (* the global M bounds (per clock) of an automaton *)
+  (* this required if you want to bound the automaton *)
+  val global_mbounds : ta -> int array
+
+  (* to load a TA from a file *)
+  val model : ta
+
+  (** PRINT FUNCTIONS **)
+  val string_of_state : ta -> state -> string
+  val print_timed_automaton : out_channel -> ta -> unit
+end
+
+(**
+ * If you want to load a compiled module, you must implement the TA
+ * interface above, and you should set this variable.
+ * E.g.
+ *    module MyTA : TA = struct ... end
+ *    let _ = Ita.loadedmodule := Some (module MyTA)
+ *
+ * It is the only way provided by the Ocaml Dynlink module to access the
+ * dynamically loaded data.
+ *)
+val loadedmodule : (module TA) option ref
+

src/timedAutomaton.ml

@@ -95,6 +95,7 @@ struct
   type timed_automaton =
     {
       t : BareTA.ta;
+      clocks : VarContext.t;
       lu_tbl : (Udbml.Carray.t * Udbml.Carray.t) DSHashtbl.t;
       m_tbl : Udbml.Carray.t DSHashtbl.t;
     }
@@ -102,7 +103,7 @@ struct
   type edge (* TODO *)
   
   (* indirection *)
-  let clocks ta = BareTA.clocks ta.t
+  let clocks ta = ta.clocks
   (* indirection *)
   let priority_compare = BareTA.priority_compare
   (* indirection *)
@@ -196,17 +197,26 @@ struct
     out "(";
     out (BareTA.string_of_state ta.t source);
     out ",";
-    out (Ita.print_guard (clocks ta) guard);
+    out (Ita.print_guard (BareTA.string_of_clock ta.t) guard);
     out ",";
-    out (Ita.print_resets (clocks ta) ulist);
+    out (Ita.print_resets (BareTA.string_of_clock ta.t) ulist);
     out ",";
     out (BareTA.string_of_state ta.t target);
     out ")";
     Buffer.contents buf
 
   let model =
+    let ta = BareTA.model in
+    let clocks = VarContext.create () in
+    (* the reference clock *)
+    let _ = VarContext.add clocks "t(0)" in
+    for i = 1 to BareTA.nb_clocks ta do
+      let j = VarContext.add clocks (BareTA.string_of_clock ta i) in
+      assert(i = j)
+    done;
     {
       t = BareTA.model;
+      clocks = clocks;
       lu_tbl = DSHashtbl.create 1024;
       m_tbl = DSHashtbl.create 1024;
     }

src/uppaalta.ml

@@ -469,6 +469,11 @@ struct
   (********** TIMED_AUTOMATON interface **********)
   let clocks ta = ta.clocks
 
+  let nb_clocks ta = VarContext.size (clocks ta)
+
+  let string_of_clock ta cl =
+    VarContext.var_of_index (clocks ta) cl
+
   let initial_state ta = ta.init
 
   let rate_of_state ta state =

src/varcontext.ml

@@ -42,7 +42,7 @@ sig
   val iter : t -> (var_t -> int -> unit) -> unit
 end
 
-module VarContextFunctor : VARCONTEXT =
+module VarContextFunctor =
   functor (Vars : sig type var_t type array_t val cell2var : array_t -> int list -> var_t end) ->
 struct
   type var_t = Vars.var_t

tests/compiled.ml

@@ -12,11 +12,15 @@ struct
   type state = int
   type ta =
     {
-      clocks : Varcontext.VarContext.t;
       init : state;
+      clocks : string array;
     }
 
-  let clocks t = t.clocks
+  (* /!\ clocks are numbered from 1 to nb_clocks *)
+  let nb_clocks t = (Array.length t.clocks)
+  let string_of_clock t c =
+    assert(c >= 1 && c <= (nb_clocks t));
+    t.clocks.(c-1)
 
   let initial_state t = t.init
 
@@ -37,18 +41,18 @@ struct
   let rate_of_state _ _ = 1
 
   let lubounds t s =
-    Array.make (Varcontext.VarContext.size t.clocks) 10,
-    Array.make (Varcontext.VarContext.size t.clocks) 10
+    Array.make (nb_clocks t) 10,
+    Array.make (nb_clocks t) 10
 
   let global_mbounds t =
-    Array.make (Varcontext.VarContext.size t.clocks) 10
+    Array.make (nb_clocks t) 10
 
   let model =
-    let cl = Varcontext.VarContext.create () in
-    let _ = Varcontext.VarContext.add cl "c0" in ();
+    let cl = Array.make 1 "" in
+    cl.(0) <- "c0";
     {
-      clocks = cl;
       init = 0;
+      clocks = cl;
     }
 
   let string_of_state _ _ = "state"