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