Commit 5de75d0f authored by Maximilien Colange's avatar Maximilien Colange

Rework Ita.TA interface for clocks, no longer uses a VarContext.

parent 1b09863b
......@@ -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
......
......@@ -13,11 +13,6 @@ type atomic_guard =
(* a guard is a conjunction of atomic guards *)
type guard_t = atomic_guard list
(* a printer for an atomic guard *)
val print_ag : Varcontext.VarContext.t -> atomic_guard -> string
(* a printer for a guard *)
val print_guard : Varcontext.VarContext.t -> guard_t -> string
(**
* a reset is a pair (c,k), where c is a clock id (see VarContext)
......@@ -25,8 +20,25 @@ val print_guard : Varcontext.VarContext.t -> guard_t -> string
*)
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 : Varcontext.VarContext.t -> reset_t list -> string
val print_resets : (int -> string) -> reset_t list -> string
(**
* The interface of Timed Automaton to implement when you want to provide
......@@ -37,8 +49,15 @@ sig
type ta
type state
(* retrieves ALL the clocks of the model *)
val clocks : ta -> Varcontext.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
......
......@@ -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;
}
......
......@@ -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 =
......
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment