Re: [tlaplus] Liveness only when a certain condition holds

Your property only asserts that if at some point there is an election and all nodes are active then eventually ElectionWorks holds. From your description it sounds like you are aiming for

[](/\ ThereIsAnElection

/\ [] EveryoneStaysActiveDuringElection

=> <> ElectionWorks)

Stephan

On 9 May 2023, at 00:29, Jones Martins <jonesmvc@xxxxxxxxx> 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/8a4e5219-e482-49b5-aa16-f31f9b673f6en%40googlegroups.com.

--
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/E251BE92-59D4-4BB5-ABE8-70A1FC631289%40gmail.com.