Re: [tlaplus] New user: question about 'with'

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

On 9 Aug 2020, at 03:20, rsharp1910@xxxxxxxxx wrote:

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.

--
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/032F36EC-DA67-4D4A-ACE7-0DDB00B724CA%40gmail.com.