Commit 872d1c1f authored by Maximilien Colange's avatar Maximilien Colange

A simple test for compiled models.

parent 4d888158
(**
* To run this test, first compile it as a .cmxs.
* The easiest way to achieve this is, from the toplevel directory of TiAMo,
* and after having compiled TiAMo, to run the command:
* ocamlbuild tests/compiled.cmxs
* To use the compiled model, run:
* ./tiamo reach _build/tests/compiled.cmxs
*)
module Test : Ita.TA =
struct
type state = int
type ta =
{
clocks : Varcontext.VarContext.t;
init : state;
}
let clocks t = t.clocks
let initial_state t = t.init
let hash_state s = s
let equal_state s1 s2 = s1 = s2
let is_target _ _ = false
let priority_compare s1 s2 = compare s1 s2
let transitions_from _ _ = []
let invariant _ _ = []
let is_urgent_or_committed _ _ = false
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
let global_mbounds t =
Array.make (Varcontext.VarContext.size t.clocks) 10
let model =
let cl = Varcontext.VarContext.create () in
let _ = Varcontext.VarContext.add cl "c0" in ();
{
clocks = cl;
init = 0;
}
let string_of_state _ _ = "state"
let print_timed_automaton chan _ = Printf.fprintf chan "dummy TA\n"
end
let _ =
Ita.loadedmodule := Some (module Test)
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