Hi. This post contains three *correlated* questions from the same code snippet attached below.
Q1. Model checking the program gives 5 states and 3 distinct ones. What are the exact states?
Q3. The tla translated code for the with statement is:
with f \in Flags do
flags[f] := TRUE;
end with;
Lbl_1 == /\ pc = "Lbl_1"
/\ \E f \in Flags:
flags' = [flags EXCEPT ![f] = TRUE]
/\ pc' = "Done"
The pcal with clause branches each possible Flags value. But the tla one, which seems to me, only works on one possible new state because of the \E (as long as there exists one) logical operator.
I must be understanding something wrong about the \E here.
Thanks.
---- MODULE simple ----
EXTENDS Integers, TLC, Sequences, FiniteSets
Flags == {"f1", "f2"}
(* --algorithm simple
variables
flags = [f \in Flags |-> FALSE];
begin
with f \in Flags do
flags[f] := TRUE;
end with;
end algorithm; *)
\* BEGIN TRANSLATION
VARIABLES flags, pc
vars == << flags, pc >>
Init == (* Global variables *)
/\ flags = [f \in Flags |-> FALSE]
/\ pc = "Lbl_1"
Lbl_1 == /\ pc = "Lbl_1"
/\ \E f \in Flags:
flags' = [flags EXCEPT ![f] = TRUE]
/\ pc' = "Done"
Next == Lbl_1
\/ (* Disjunct to prevent deadlock on termination *)
(pc = "Done" /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(pc = "Done")
\* END TRANSLATION
====