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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 10 Apr 2019 14:59:12 +0200*References*: <2cffcbe8-ade6-4f43-bd5a-bd90896dbd66@googlegroups.com>

Expanding the operator definition for the two actions produces (1) \E y \in {x} : x' = ~ y \* for "ThisAdvances" and (2) \E y \in {x} : y' = ~ y \* for "ThisDeadlocks" Evaluating (1) in the initial state where x = TRUE yields (1') \E y \in {TRUE} : x' = ~ y which is true for the successor state in which x = FALSE, so this will be the new state constructed by TLC. In contrast, when evaluating (2), observe that the quantifiers \A and \E bind values ("constants" in TLA+ jargon), therefore y' reduces to y (just as 42' reduces to 42) and therefore we get (2') \E y \in {TRUE} : y = ~ y which evaluates to FALSE, hence no new state satisfying this formula can be constructed. 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout. |

**Follow-Ups**:**Re: [tlaplus] Priming variables from "exists in" expressions?***From:*Branen Salmon

**References**:**[tlaplus] Priming variables from "exists in" expressions?***From:*Branen Salmon

- Prev by Date:
**[tlaplus] Priming variables from "exists in" expressions?** - Next by Date:
**Re: [tlaplus] Priming variables from "exists in" expressions?** - Previous by thread:
**[tlaplus] Priming variables from "exists in" expressions?** - Next by thread:
**Re: [tlaplus] Priming variables from "exists in" expressions?** - Index(es):