--
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/8a4e5219-e482-49b5-aa16-f31f9b673f6en%40googlegroups.com.
I'd suggest a slightly different way of doing the same thing:
Next2 == Next /\ EveryoneStaysActiveDuringElection'
Spec2 == Init /\ [][Next2]_vars /\ Fairness
As for the initial problem, I think it's because EveryoneStaysActiveDuringElection is true when there isn't an election or if no nodes are part of the election, which the new version doesn't have. Maybe that's part of it?
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/55724505-e203-4176-a2c8-72a1d95ef0f3n%40googlegroups.com.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/EO9ff0OBqtA/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d49bbe36-1f70-545f-b251-7757e342f07c%40gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/baea1ec0-47a0-42b5-b250-20938dedac5fn%40googlegroups.com.