2019-12-03 21:48:57 +08:00
|
|
|
EXTENDS TLC
|
|
|
|
|
|
|
|
|
|
(* --algorithm hello_world
|
|
|
|
|
variable s \in {"Hello", "World!"};
|
|
|
|
|
begin
|
|
|
|
|
A:
|
|
|
|
|
print s;
|
2019-12-03 21:49:48 +08:00
|
|
|
end algorithm; *)
|
|
|
|
|
\* BEGIN TRANSLATION
|
|
|
|
|
VARIABLES s, pc
|
|
|
|
|
|
|
|
|
|
vars == << s, pc >>
|
|
|
|
|
|
|
|
|
|
Init == (* Global variables *)
|
|
|
|
|
/\ s \in {"Hello", "World!"}
|
|
|
|
|
/\ pc = "A"
|
|
|
|
|
|
|
|
|
|
A == /\ pc = "A"
|
|
|
|
|
/\ PrintT(s)
|
|
|
|
|
/\ pc' = "Done"
|
|
|
|
|
/\ s' = s
|
|
|
|
|
|
|
|
|
|
(* Allow infinite stuttering to prevent deadlock on termination. *)
|
|
|
|
|
Terminating == pc = "Done" /\ UNCHANGED vars
|
|
|
|
|
|
|
|
|
|
Next == A
|
|
|
|
|
\/ Terminating
|
|
|
|
|
|
|
|
|
|
Spec == Init /\ [][Next]_vars
|
|
|
|
|
|
|
|
|
|
Termination == <>(pc = "Done")
|
|
|
|
|
|
|
|
|
|
\* END TRANSLATION
|
