Commit 36d8b097 authored by Maximilien Colange's avatar Maximilien Colange

Add a .mli for compiled TA interface.

parent 872d1c1f
(**
* 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 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)
* and k is a constant.
*)
type reset_t = Common.clock_t * int
(* a printer for a list of resets *)
val print_resets : Varcontext.VarContext.t -> 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
(* retrieves ALL the clocks of the model *)
val clocks : ta -> Varcontext.VarContext.t
(* 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
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