Commit 269e7e8b authored by Maximilien Colange's avatar Maximilien Colange

Fix the way the reference clock is handled.

parent 39e824e0
...@@ -208,16 +208,13 @@ struct ...@@ -208,16 +208,13 @@ struct
let model = let model =
let ta = BareTA.model in let ta = BareTA.model in
let clocks = VarContext.create () in let clocks = VarContext.create () in
(* the reference clock *)
let i0 = VarContext.add clocks "t(0)" in
assert(i0 = 0);
for i = 1 to BareTA.nb_clocks ta do for i = 1 to BareTA.nb_clocks ta do
let j = VarContext.add clocks (BareTA.string_of_clock ta i) in let j = VarContext.add clocks (BareTA.string_of_clock ta i) in
assert(i = j) assert(i = j)
done; 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; t = BareTA.model;
clocks = clocks; clocks = clocks;
......
...@@ -475,11 +475,11 @@ struct ...@@ -475,11 +475,11 @@ struct
(********** TIMED_AUTOMATON interface **********) (********** TIMED_AUTOMATON interface **********)
let clocks ta = ta.clocks let clocks ta = ta.clocks
let nb_clocks ta = VarContext.size (clocks ta) let nb_clocks ta = (VarContext.size (clocks ta))-1
let string_of_clock ta cl = let string_of_clock ta cl =
assert(cl > 0 && cl <= nb_clocks ta); assert(cl > 0 && cl <= VarContext.size (clocks ta));
VarContext.var_of_index (clocks ta) (cl-1) VarContext.var_of_index (clocks ta) cl
let initial_state ta = ta.init 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