Commit d3c9d422 authored by Ocan Sankur's avatar Ocan Sankur

added support for boolean variable through ints

parent 3bc6a90b
type expression =
| Constant of int
| Variable of int
| Not of expression
| ConstVariable of int
| Clock of int
| ClockArray of int * expression list
......@@ -10,3 +11,5 @@ type expression =
| Product of expression * expression
| Substraction of expression * expression
| Division of expression * expression
| And of expression * expression
| Eq of expression * expression
......@@ -91,8 +91,7 @@ let main() =
Options.symbolic_verify (module MC)
(*
printf "Checking result with explicit engine:\n"; flush stdout;
Options.verify (module MC)
*)
Options.verify (module MC)*)
)
in
Printf.printf "Result of verification is %s\n" res;
......
open Expression
open Printf
type atomic_guard =
type atomic_guard =
| GuardLeq of expression * expression
| GuardLess of expression * expression
| GuardGeq of expression * expression
| GuardGreater of expression * expression
| GuardEqual of expression * expression
| GuardNeq of expression * expression
let string_of_exp = function
| GuardNot of atomic_guard
| GuardIdentifier of expression
let rec string_of_exp = function
|Constant(c) -> sprintf "%d" c
|Variable(i) -> sprintf "V(%d)" i
|_ -> failwith "not implemented"
|Not(e) -> sprintf "!%s" (string_of_exp e)
|Clock(x) -> sprintf "Clock(%d)" x
|And(x,y) -> sprintf "(%s & %s)" (string_of_exp x) (string_of_exp y)
| _ -> "not implemented"
let string_of_atomic_guard =
let rec string_of_atomic_guard =
function
| GuardLeq(v,exp) ->
sprintf "%s <= %s" (string_of_exp v)(string_of_exp exp)
......@@ -27,6 +33,10 @@ let string_of_atomic_guard =
sprintf "%s == %s" (string_of_exp v) (string_of_exp exp)
| GuardNeq(v,exp)->
sprintf "%s != %s" (string_of_exp v) (string_of_exp exp)
| GuardNot(g) ->
sprintf "!(%s)" (string_of_atomic_guard g)
| GuardIdentifier(exp) ->
sprintf "%s" (string_of_exp exp)
(** Atomic guard factory functions, to be registered as callbacks from C *)
(** This ensures that guards are in normal form GuardXX(Clock(_),_) *)
......@@ -50,6 +60,13 @@ let cb_atomic_guard_NEQ a = function
| Clock(_) | ClockArray(_,_) as b -> GuardNeq(b, a)
| _ as b -> GuardNeq(a,b)
let cb_atomic_guard_NOT a = GuardNot a
let cb_atomic_guard_ID = function
| Clock(_) | ClockArray(_,_) ->
failwith "Cannot use clocks as guard predicates"
| a -> GuardNeq(a, (Constant 0))
type query =
| EmptyQuery
| QueryAnd of query*query
......@@ -88,7 +105,7 @@ let _ =
Callback.register "cb_qb_make_and" make_query_and;
Callback.register "cb_qb_make_or" make_query_or;
Callback.register "cb_qb_make_atomic" make_query_atomic
let _ =
Callback.register "cb_print_guard" cb_print_guard;
Callback.register "cb_print_query" cb_print_query;
......@@ -98,7 +115,9 @@ let _ =
Callback.register "cb_atomic_guard_GE" cb_atomic_guard_GE;
Callback.register "cb_atomic_guard_GT" cb_atomic_guard_GT;
Callback.register "cb_atomic_guard_EQ" cb_atomic_guard_EQ;
Callback.register "cb_atomic_guard_NEQ" cb_atomic_guard_NEQ
Callback.register "cb_atomic_guard_NEQ" cb_atomic_guard_NEQ;
Callback.register "cb_atomic_guard_NOT" cb_atomic_guard_NOT;
Callback.register "cb_atomic_guard_ID" cb_atomic_guard_ID
......
......@@ -392,14 +392,13 @@ struct
let rec expand_state ta state =
let (loc, zone, _) = WO.State.get state in
(*
(*
printf "Expanding following state\n";
TA.print_extended_state Pervasives.stdout ta (loc, zone);
printf "of depth: %d" (WO.State.depth state);
printf "\n";
flush stdout;
*)
*)
(* retrieve the transitions out of 'loc' *)
let transition_list =
try
......@@ -534,14 +533,29 @@ struct
if (!print_path) then
let rec aux = fun state ->
let father = WO.State.father state in
let (loc,_,_) = WO.State.get father in
printf "Father:\n";
TA.print_discrete_state Pervasives.stdout ta loc;
printf "\n";
printf "of depth: %d\n" (WO.State.depth father);
let (loc,_,_) = WO.State.get state in
printf "Child:\n";
TA.print_discrete_state Pervasives.stdout ta loc;
printf "\n";
printf "of depth: %d\n" (WO.State.depth state);
if father == WO.State.root then(
""
) else (
try
printf "Parent has %d children\n" (List.length (WO.State.sons father));
let (g,r,_) = List.find (fun (_,_,x) -> x == state) (WO.State.sons father) in
let (source,_,_) = WO.State.get father in
let (target,_,_) = WO.State.get state in
(aux father) ^ "\n" ^ (TA.transition_to_string ta (source, g, r, target))
printf "TRANS:\n%s\n" (TA.transition_to_string ta (source, g, r, target));
(aux father) ^ "\n" ^ (TA.transition_to_string ta (source, g, r, target))
with Not_found ->
failwith "[ERR] Transition could not be found\n";
)
......
......@@ -49,6 +49,9 @@ struct
(* to be called when a state is subsumed: mark all successors as subsumed
* as well, exploiting the WSTS property.
FIXME: This makes the generation of witnesses fail.
We should also store the subsuming node so that a witness can be generated.
*)
let rec subsume str_of_state s =
(* mark all its successors as subsumed *)
......@@ -63,8 +66,8 @@ struct
let add_sons s l =
s.sons <- l @ s.sons
(* for debugging:
List.iter (fun (_,_,x) ->
(* for debugging:
List.iter (fun (_,_,x) ->
try
ignore(List.find (fun (_,_,x') -> x == x') s.sons)
with Not_found ->
......
......@@ -490,9 +490,9 @@ constraints (x,y,_) with x>y"
List.iter (fun ag -> approximate (BTA.ag_to_pair ag)) g;
And (Queue.fold (fun acc x -> x :: acc) [] cube)
let smv_string_of_atomic_guard bta =
let rec smv_string_of_atomic_guard bta =
let open BTA in
let string_of_exp = string_of_exp bta in
let string_of_exp = string_of_exp bta ~equal_sign:"=" in
function
| GuardLeq(v,exp) ->
sprintf "%s <= %s" (string_of_exp v)(string_of_exp exp)
......@@ -503,9 +503,11 @@ constraints (x,y,_) with x>y"
| GuardGreater(v,exp)->
sprintf "%s > %s" (string_of_exp v) (string_of_exp exp)
| GuardEqual(v,exp)->
sprintf "%s = %s" (string_of_exp v) (string_of_exp exp)
sprintf "toint(%s) = toint(%s)" (string_of_exp v) (string_of_exp exp)
| GuardNeq(v,exp)->
sprintf "%s != %s" (string_of_exp v) (string_of_exp exp)
sprintf "toint(%s) != toint(%s)" (string_of_exp v) (string_of_exp exp)
| GuardNot(exp) ->
sprintf "toint(!tobool(%s))" (smv_string_of_atomic_guard bta exp)
let rec smv_string_of_syntactic_guard bta g =
let rec aux = function
......@@ -997,7 +999,7 @@ constraints (x,y,_) with x>y"
) e.edgeUpdates in
let upexpr = List.assoc (Variable vi) updates_w_exp in
let upstr = string_of_exp bta upexpr in
fprintf out "\t\tmode = reset & e1 = %d & %d <= %s & %s <= %d : %s;\n"
fprintf out "\t\tmode = reset & e1 = %d & %d <= toint(%s) & toint(%s) <= %d : toint(%s);\n"
(EdgeIndexer.get_index edgeIndexer e) l upstr upstr r upstr
);
s_edges
......@@ -1014,7 +1016,7 @@ constraints (x,y,_) with x>y"
in
(** If both edges update the variable, the receiving edge has priority *)
let upstr = string_of_exp bta upexpr in
fprintf out "\t\tmode = reset & e1 = %d & e2 = %d & %d <= %s & %s <= %d : %s;\n"
fprintf out "\t\tmode = reset & e1 = %d & e2 = %d & %d <= toint(%s) & toint(%s) <= %d : toint(%s);\n"
(EdgeIndexer.get_index edgeIndexer e1)
(EdgeIndexer.get_index edgeIndexer e2)
l upstr
......
This diff is collapsed.
......@@ -17,6 +17,8 @@ sig
| GuardGreater of Expression.expression * Expression.expression
| GuardEqual of Expression.expression * Expression.expression
| GuardNeq of Expression.expression * Expression.expression
| GuardNot of Querybuilder.atomic_guard
| GuardIdentifier of Expression.expression
type guard = atomic_guard list
type lvalue =
ClockRef of Common.clock_t
......@@ -120,7 +122,7 @@ sig
global_mbounds : int array;
}
val string_of_exp :
ta -> Expression.expression -> Varcontext.VarContext.arr_t
ta -> ?equal_sign: string -> Expression.expression -> Varcontext.VarContext.arr_t
val string_of_atomic_guard : ta -> atomic_guard -> string
val xml_string_of_atomic_guard : ta -> atomic_guard -> string
val string_of_guard : ta -> atomic_guard list -> string
......@@ -257,6 +259,11 @@ struct
let cb_expression_product a b = Product (a,b)
let cb_expression_substraction a b = Substraction (a,b)
let cb_expression_division a b = Division (a,b)
let cb_expression_not a = Not a
let cb_expression_and a b = And(a,b)
let cb_expression_eq a b = Eq(a,b)
let cb_expression_neq a b = Not(Eq(a,b))
(** A guard is a conjunction of atomic guards *)
type guard = atomic_guard list
......@@ -388,7 +395,7 @@ struct
}
(********** PRINTING AUXILIARY FUNCTIONS **********)
let rec string_of_exp ta e =
let rec string_of_exp ta ?equal_sign:(equal_sign="==") e =
let string_of_exp = string_of_exp ta in
(function
| Constant c -> sprintf "%d" c
......@@ -419,6 +426,14 @@ struct
| Substraction(e1,e2) ->
sprintf "(%s - %s)" (string_of_exp e1)
(string_of_exp e2)
| Not(e) ->
sprintf "!%s" (string_of_exp e)
| And(e1,e2) ->
sprintf "(%s & %s)" (string_of_exp e1)
(string_of_exp e2)
| Eq(e1,e2) ->
(* sprintf "(%s %s %s)" (string_of_exp e1) equal_sign (string_of_exp e2)*)
sprintf "(%s = %s)" (string_of_exp e1) (string_of_exp e2)
) e
......@@ -437,6 +452,10 @@ struct
sprintf "%s == %s" (string_of_exp v) (string_of_exp exp)
| GuardNeq(v,exp)->
sprintf "%s != %s" (string_of_exp v) (string_of_exp exp)
| GuardNot(exp)->
sprintf "!(%s)" (string_of_atomic_guard exp)
| GuardIdentifier(exp)->
sprintf "%s" (string_of_exp exp)
let xml_string_of_atomic_guard ta =
......@@ -454,6 +473,10 @@ struct
sprintf "%s == %s" (string_of_exp v) (string_of_exp exp)
| GuardNeq(v,exp)->
sprintf "%s != %s" (string_of_exp v) (string_of_exp exp)
| GuardNot(exp)->
sprintf "!(%s)" (string_of_atomic_guard ta exp)
| GuardIdentifier(exp)->
sprintf "%s" (string_of_exp exp)
let rec string_of_guard ta =
......@@ -598,6 +621,18 @@ struct
| Sum(e1,e2) -> Constant ((eval_disc_exp ta vars e1) + (eval_disc_exp ta vars e2))
| Division(e1,e2) -> Constant ((eval_disc_exp ta vars e1) / (eval_disc_exp ta vars e2))
| Substraction(e1,e2) -> Constant ((eval_disc_exp ta vars e1) - (eval_disc_exp ta vars e2))
| Not(e) -> if (eval_disc_exp ta vars e) = 1 then Constant 0
else Constant 1
| And(e1,e2) ->
let c1 = (eval_disc_exp ta vars e1) in
let c2 = (eval_disc_exp ta vars e2) in
if c1 = 0 || c2 = 0 then Constant 0
else Constant 1
| Eq(e1,e2) ->
let c1 = (eval_disc_exp ta vars e1) in
let c2 = (eval_disc_exp ta vars e2) in
if c1 == c2 then Constant 1 else Constant 0
(* same as above, but fails if it encounters a clock *)
and eval_disc_exp ta vars exp =
match (eval_exp ta vars exp) with
......@@ -611,7 +646,7 @@ struct
(* evaluate the discrete part of a guard
* the result contains only clocks and constants (no clock array, no expression)
*)
let eval_ag ta state ag =
let rec eval_ag ta state ag =
let eval = eval_exp ta state.stateVars in
match ag with
| GuardLeq(a,b) -> GuardLeq(eval a, eval b)
......@@ -620,10 +655,12 @@ struct
| GuardNeq(a,b) -> GuardNeq(eval a, eval b)
| GuardGeq(a,b) -> GuardGeq(eval a, eval b)
| GuardGreater(a,b) -> GuardGreater(eval a, eval b)
| GuardNot(a) -> GuardNot (eval_ag ta state a)
| GuardIdentifier(a) -> GuardIdentifier a
(* completely evaluate a discrete guard to true or false.
* fails if it encounters a clock *)
let eval_disc_guard ta state =
let rec eval_disc_guard ta state =
List.for_all (fun x ->
match eval_ag ta state x with
| GuardLeq(Constant(a),Constant(b)) -> a <= b
......@@ -632,6 +669,7 @@ struct
| GuardNeq(Constant(a),Constant(b)) -> a <> b
| GuardGeq(Constant(a),Constant(b)) -> a >= b
| GuardGreater(Constant(a),Constant(b)) -> a > b
| GuardNot(a) -> not (eval_disc_guard ta state [a])
| _ -> failwith "Unevaluable discrete guard")
let is_committed state =
......@@ -977,9 +1015,19 @@ struct
loc.compExpr.(cl) <- lnew, unew
)
(clocks_of ta lhs)
| _ ->
| GuardNeq(lhs,e) ->
failwith "LU: GuardNeq"
| GuardNot(g) ->
failwith "LU: GuardNot"
| GuardIdentifier(g) ->
failwith "LU: Id"
(*
| g ->
Log.fatal (sprintf "The following guard is the problem: %s\n"
(string_of_atomic_guard ta g));
failwith
"cannot compute LU bounds, guard is not in normal form"
*)
in
(* add invariant contribution *)
......@@ -1151,6 +1199,7 @@ struct
(* Register C callbacks to build expressions *)
Callback.register "cb_expression_constant" cb_expression_constant;
Callback.register "cb_expression_not" cb_expression_not;
Callback.register "cb_expression_variable"
(cb_expression_variable constcont const_values varcont);
Callback.register "cb_expression_clock" (cb_expression_clock clockcont);
......@@ -1158,6 +1207,9 @@ struct
Callback.register "cb_expression_product" cb_expression_product;
Callback.register "cb_expression_substraction" cb_expression_substraction;
Callback.register "cb_expression_division" cb_expression_division;
Callback.register "cb_expression_and" cb_expression_and;
Callback.register "cb_expression_eq" cb_expression_eq;
Callback.register "cb_expression_neq" cb_expression_neq;
Callback.register "cb_expression_array"
(cb_expression_array varcont constcont clockcont);
......@@ -1256,6 +1308,10 @@ struct
| Product(a,b) -> (evaluate_expression a) * (evaluate_expression b)
| Substraction(a,b) -> (evaluate_expression a) - (evaluate_expression b)
| Division(a,b) -> (evaluate_expression a) / (evaluate_expression b)
| Not(a) -> if evaluate_expression a = 1 then 0 else 1
| And(a,b) -> if (evaluate_expression a <> 0) && (evaluate_expression b <> 0) then 1
else 0
| Eq(a,b) -> if (evaluate_expression a = evaluate_expression b) then 1 else 0
in
Callback.register "cb_evaluate_expr" evaluate_expression;
(** Get discrete guard from mixed guard *)
......@@ -1269,13 +1325,15 @@ struct
| Array(_, l) -> List.for_all (fun x -> filt_exp x) l
| _ -> true
in
let filt_ag = function
let rec filt_ag = function
| GuardLess(x,y) -> (filt_exp x) && (filt_exp y)
| GuardLeq(x,y) -> (filt_exp x) && (filt_exp y)
| GuardGreater(x,y) -> (filt_exp x) && (filt_exp y)
| GuardGeq(x,y) -> (filt_exp x) && (filt_exp y)
| GuardEqual(x,y) -> (filt_exp x) && (filt_exp y)
| GuardNeq(x,y) -> (filt_exp x) && (filt_exp y)
| GuardNot(x) -> filt_ag x
| GuardIdentifier(x) -> (filt_exp x)
in
List.filter filt_ag g
in
......@@ -1290,13 +1348,15 @@ struct
| Array(_, l) -> List.exists (fun x -> filt_exp x) l
| _ -> false
in
let filt_ag = function
let rec filt_ag = function
| GuardLess(x,y) -> (filt_exp x) || (filt_exp y)
| GuardLeq(x,y) -> (filt_exp x) || (filt_exp y)
| GuardGreater(x,y) -> (filt_exp x) || (filt_exp y)
| GuardGeq(x,y) -> (filt_exp x) || (filt_exp y)
| GuardEqual(x,y) -> (filt_exp x) || (filt_exp y)
| GuardNeq(x,y) -> (filt_exp x) || (filt_exp y)
| GuardNot(x) -> false
| GuardIdentifier(x) -> false
in
List.filter filt_ag g
in
......@@ -1364,7 +1424,8 @@ struct
{ ta with query = newquery; }
in
Callback.register "cb_set_query" ta_set_query;
utap_from_file tafile qfile
let r = utap_from_file tafile qfile in
r
(** Returns a table t where t.(x).(y) is the array of constants k
appearing as x-y<=k or x-y<k in the automaton *)
......
......@@ -11,7 +11,7 @@ clock x,y;</declaration><template><name x="5" y="5">Task1</name><declaration>//
const int T = 4;
const int D = 3;
const int C = 1;</declaration><location id="id0" x="-112" y="-232"><name x="-122" y="-262">pause</name></location><location id="id1" x="152" y="-56"><name x="142" y="-86">running</name><label kind="invariant" x="142" y="-41">y&lt;=C</label></location><location id="id2" x="-16" y="-56"><name x="-26" y="-86">wait</name></location><location id="id3" x="-152" y="-56"><name x="-162" y="-86">idle</name></location><init ref="id3"/><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="-40" y="-159">pause1?</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="synchronisation" x="-124" y="-159">pause1?</label></transition><transition><source ref="id3"/><target ref="id0"/><label kind="synchronisation" x="-192" y="-159">pause1?</label></transition><transition><source ref="id3"/><target ref="id3"/><label kind="assignment" x="-212" y="-56">x:=0, y:=0</label><nail x="-256" y="-104"/><nail x="-216" y="-128"/></transition><transition><source ref="id3"/><target ref="id3"/><label kind="guard" x="-424" y="-64">y==0 &amp;&amp; x&gt;=D</label><label kind="synchronisation" x="-368" y="-48">error!</label><nail x="-248" y="-56"/><nail x="-248" y="8"/></transition><transition><source ref="id1"/><target ref="id3"/><label kind="guard" x="16" y="48">y&lt;=C</label><label kind="synchronisation" x="8" y="32">finished!</label><label kind="assignment" x="24" y="64">y:=0</label><nail x="272" y="-56"/><nail x="272" y="24"/><nail x="-152" y="24"/></transition><transition><source ref="id2"/><target ref="id2"/><label kind="guard" x="-24" y="-152">x&gt;=D</label><label kind="synchronisation" x="-32" y="-176">error!</label><nail x="-56" y="-152"/><nail x="56" y="-152"/></transition><transition><source ref="id2"/><target ref="id1"/><label kind="synchronisation" x="56" y="-80">go1?</label><label kind="assignment" x="64" y="-56">y:=0</label></transition><transition><source ref="id3"/><target ref="id2"/><label kind="guard" x="-128" y="-72">x&gt;= T</label><label kind="synchronisation" x="-120" y="-88">ready!</label><label kind="assignment" x="-120" y="-48">x:=0, waiting1:=true</label></transition></template><template><name x="5" y="5">Task2</name><declaration>// Place local declarations here.
const int C = 1;</declaration><location id="id0" x="-112" y="-232"><name x="-122" y="-262">pause</name></location><location id="id1" x="152" y="-56"><name x="142" y="-86">running</name><label kind="invariant" x="142" y="-41">y&lt;=C</label></location><location id="id2" x="-16" y="-72"><name x="-26" y="-102">wait</name></location><location id="id3" x="-152" y="-56"><name x="-162" y="-86">idle</name></location><init ref="id3"/><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="-40" y="-159">pause1?</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="synchronisation" x="-124" y="-159">pause1?</label></transition><transition><source ref="id3"/><target ref="id0"/><label kind="synchronisation" x="-192" y="-159">pause1?</label></transition><transition><source ref="id3"/><target ref="id3"/><label kind="assignment" x="-272" y="-136">x:=0, y:=0</label><nail x="-256" y="-104"/><nail x="-216" y="-128"/></transition><transition><source ref="id3"/><target ref="id3"/><label kind="guard" x="-424" y="-64">y==0 &amp;&amp; x&gt;=D</label><label kind="synchronisation" x="-368" y="-48">error!</label><nail x="-248" y="-56"/><nail x="-248" y="8"/></transition><transition><source ref="id1"/><target ref="id3"/><label kind="guard" x="16" y="48">y&lt;=C</label><label kind="synchronisation" x="8" y="32">finished!</label><label kind="assignment" x="24" y="64">y:=0</label><nail x="272" y="-56"/><nail x="272" y="24"/><nail x="-152" y="24"/></transition><transition><source ref="id2"/><target ref="id2"/><label kind="guard" x="0" y="-184">x&gt;=D</label><label kind="synchronisation" x="0" y="-200">error!</label><nail x="-56" y="-168"/><nail x="56" y="-168"/></transition><transition><source ref="id2"/><target ref="id1"/><label kind="synchronisation" x="56" y="-80">go1?</label><label kind="assignment" x="64" y="-56">y:=0</label></transition><transition><source ref="id3"/><target ref="id2"/><label kind="guard" x="-128" y="-72">x&gt;= T</label><label kind="synchronisation" x="-120" y="-88">ready!</label><label kind="assignment" x="-120" y="-48">x:=0, waiting1:=true</label></transition></template><template><name x="5" y="5">Task2</name><declaration>// Place local declarations here.
clock x;
clock y;
const int T = 2;
......@@ -21,7 +21,7 @@ clock x;
clock y;
const int T = 5;
const int D = 1;
const int C = 1;</declaration><location id="id7" x="152" y="-56"><name x="142" y="-86">running</name><label kind="invariant" x="142" y="-41">y&lt;=C</label></location><location id="id8" x="-16" y="-56"><name x="-26" y="-86">wait</name></location><location id="id9" x="-152" y="-56"><name x="-162" y="-86">idle</name></location><init ref="id9"/><transition><source ref="id9"/><target ref="id9"/><label kind="assignment" x="-212" y="-56">x:=0, y:=0</label><nail x="-184" y="-184"/><nail x="-128" y="-184"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="guard" x="-212" y="-86">y==0 &amp;&amp; x&gt;=D</label><label kind="synchronisation" x="-212" y="-71">error!</label><nail x="-288" y="-56"/><nail x="-288" y="-8"/></transition><transition><source ref="id7"/><target ref="id9"/><label kind="guard" x="16" y="48">y&lt;=C</label><label kind="synchronisation" x="8" y="32">finished!</label><nail x="272" y="-56"/><nail x="272" y="24"/><nail x="-152" y="24"/></transition><transition><source ref="id8"/><target ref="id8"/><label kind="guard" x="-24" y="-152">x&gt;=D</label><label kind="synchronisation" x="-32" y="-176">error!</label><nail x="-56" y="-152"/><nail x="56" y="-152"/></transition><transition><source ref="id8"/><target ref="id7"/><label kind="synchronisation" x="56" y="-80">go3?</label><label kind="assignment" x="56" y="-56">y:=0</label></transition><transition><source ref="id9"/><target ref="id8"/><label kind="guard" x="-120" y="-80">x&gt;= T</label><label kind="synchronisation" x="-112" y="-96">ready!</label><label kind="assignment" x="-112" y="-56">x:=0, waiting3:=true</label></transition></template><template><name x="5" y="5">Task4</name><declaration>// Place local declarations here.
const int C = 1;</declaration><location id="id7" x="312" y="-32"><name x="302" y="-62">running</name><label kind="invariant" x="302" y="-17">y&lt;=C</label></location><location id="id8" x="80" y="-96"><name x="72" y="-136">wait</name></location><location id="id9" x="-152" y="-56"><name x="-162" y="-86">idle</name></location><init ref="id9"/><transition><source ref="id9"/><target ref="id9"/><label kind="assignment" x="-192" y="-200">x:=0, y:=0</label><nail x="-184" y="-184"/><nail x="-128" y="-184"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="guard" x="-328" y="0">y==0 &amp;&amp; x&gt;=D</label><label kind="synchronisation" x="-336" y="-24">error!</label><nail x="-288" y="-56"/><nail x="-288" y="-8"/></transition><transition><source ref="id7"/><target ref="id9"/><label kind="guard" x="16" y="48">y&lt;=C</label><label kind="synchronisation" x="8" y="32">finished!</label><nail x="304" y="40"/><nail x="272" y="24"/><nail x="-152" y="24"/></transition><transition><source ref="id8"/><target ref="id8"/><label kind="guard" x="72" y="-192">x&gt;=D</label><label kind="synchronisation" x="64" y="-216">error!</label><nail x="40" y="-192"/><nail x="152" y="-192"/></transition><transition><source ref="id8"/><target ref="id7"/><label kind="synchronisation" x="144" y="-88">go3?</label><label kind="assignment" x="184" y="-88">y:=0</label></transition><transition><source ref="id9"/><target ref="id8"/><label kind="guard" x="-120" y="-80">x&gt;= T</label><label kind="synchronisation" x="-112" y="-96">ready!</label><label kind="assignment" x="-80" y="-64">x:=0, waiting3:=true</label></transition></template><template><name x="5" y="5">Task4</name><declaration>// Place local declarations here.
clock x;
clock y;
const int T = 2;
......
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