The following example is from page 53 of Practical TLA+. The 'with' _expression_ supposedly causes the system to check both values of
Flags but the TLA+ is apparently only checking one. More specifically, why does TLA+ use \E and not \A here?
Flags == {"f1", "f2"}
(*--algorithm test99
variables
flags = [f \in Flags |-> FALSE];
begin
with f \in Flags do
flags[f] := TRUE;
end with;
end algorithm;*)
\* BEGIN TRANSLATION - the hash of the PCal code: PCal-34b615cacbb07515f37db511236d019e
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"
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == Lbl_1
\/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(pc = "Done")