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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 12 Aug 2020 14:06:33 +0200*References*: <1e4823c4-9a92-46e5-88a7-f6593f760558o@googlegroups.com>

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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/032F36EC-DA67-4D4A-ACE7-0DDB00B724CA%40gmail.com. |

**References**:**[tlaplus] New user: question about 'with'***From:*rsharp1910

- Prev by Date:
**Re: [tlaplus] How do you write a literal function?** - Next by Date:
**[tlaplus] Re: New user: question about 'with'** - Previous by thread:
**[tlaplus] New user: question about 'with'** - Next by thread:
**[tlaplus] Re: New user: question about 'with'** - Index(es):