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

*From*: Hillel Wayne <hwayne@xxxxxxxxx>*Date*: Wed, 8 May 2019 15:45:54 -0500*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1

Let's say we have three "blinkers", which flip between
If I want to change one of the blinkers per step, I can do it the usual way:
But what if I want to change
\/ f' = [x \in 1..3 |-> IF x \in set THEN ~f[x] ELSE f[x]]\* orNext == /\ \E set \in SUBSET (1..3):\/ f' = [x \in set |-> ~f[x]] @@ f So why can't we just do this? Because it doesn't fully specify But there's a trick we can use: the first time TLC encounters
encounters a primed variable, it uses that the generate the
potential next-states for that variable. We need to write either
This works, as it fully defines H 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. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1178a27b-9a02-56a7-4708-5079c9eaec24%40gmail.com. For more options, visit https://groups.google.com/d/optout. |

- Prev by Date:
**Re: [tlaplus] What is the purpose of THEOREM in AsynchInterface?** - Next by Date:
**[tlaplus] Re: [Noob] veiled passage in "Consensus on Transaction Commit"** - Previous by thread:
**[tlaplus] Re: Embedding TLA+ in Latex** - Next by thread:
**[tlaplus] running TLC on module imported with a parameterized INSTANCE** - Index(es):