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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Mon, 8 May 2023 20:24:28 -0700 (PDT)*References*: <8a4e5219-e482-49b5-aa16-f31f9b673f6en@googlegroups.com>

Does the same thing happen when using the "leads to" operator P ~> Q instead of P => <>Q?

Andrew

On Monday, May 8, 2023 at 6:29:29 PM UTC-4 Jones Martins wrote:

Hi everyone,I'm trying to verify the following property:ThereIsAnElection ==

\E node \in NodeSet:

InElection(node)EveryoneStaysActiveDuringElection ==

(\A node \in NodeSet:

InElection(node) => isActive[node])Property ==

[](

(/\ ThereIsAnElection

/\ EveryoneStaysActiveDuringElection) =>

<>ElectionWorks

)Which means that an election only works if no node fails during it. Yet, TLC shows me counterexamples where 'EveryoneStaysActiveDuringElection' is false. I thought that, by including it as a condition, it wouldn't appear in a counterexample. For example, I expected TLC would only show me a counterexample to Property if both ThereIsAnElection and EveryoneStaysActiveDuringElection were TRUE, but <>ElectionWorks were FALSE.Is there something wrong in my reasoning?Best,Jones

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/f7c55d5b-84cc-4fe5-986d-55921ac7fa4dn%40googlegroups.com.

**References**:**[tlaplus] Liveness only when a certain condition holds***From:*Jones Martins

- Prev by Date:
**[tlaplus] Liveness only when a certain condition holds** - Next by Date:
**Re: [tlaplus] Liveness only when a certain condition holds** - Previous by thread:
**[tlaplus] Liveness only when a certain condition holds** - Next by thread:
**Re: [tlaplus] Liveness only when a certain condition holds** - Index(es):