Commit aeeefb7c authored by Maximilien Colange's avatar Maximilien Colange

Fix the way the reference clock is declared.

This fixes a bug introduced with the dynamic loading of models.
parent 2c2b7467
......@@ -208,12 +208,16 @@ struct
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;
(* the reference clock *)
let _ =
try
VarContext.add clocks "t(0)"
with Var_already_defined -> -1 (* OK, uppaalta already defines t(0) *)
in
{
t = BareTA.model;
clocks = clocks;
......
......@@ -472,7 +472,8 @@ struct
let nb_clocks ta = VarContext.size (clocks ta)
let string_of_clock ta cl =
VarContext.var_of_index (clocks ta) cl
assert(cl > 0 && cl <= nb_clocks ta);
VarContext.var_of_index (clocks ta) (cl-1)
let initial_state ta = ta.init
......
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