New user: question about 'with'

[rshar...@gmail.com]

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

[Stephan Merz]

Lbl_1 allows the system to take two different transitions from the initial state, one per flag value, and TLC will check both of these transitions (cf. the number of distinct states that TLC reports).

Another way to understand this is that the existential quantifier occurs on the left of the implication of a putative theorem

Spec => Property

(where by default Property checks absence of deadlock), and therefore has universal force according to the law of logic that asserts the equivalence of

(\E x \in S : F) => G   and   \A x \in S : (F => G)

when x doesn't occur in G.

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1e4823c4-9a92-46e5-88a7-f6593f760558o%40googlegroups.com.

[Ray Sharp]

Thanks for the reply, it helped.