[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] New user: question about 'with'



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")

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1e4823c4-9a92-46e5-88a7-f6593f760558o%40googlegroups.com.