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

[tlaplus] Liveness only when a certain condition holds

Hi everyone,

I'm trying to verify the following property:

ThereIsAnElection ==
  \E node \in NodeSet:

EveryoneStaysActiveDuringElection ==
  (\A node \in NodeSet:
      InElection(node) => isActive[node])

Property ==
    (/\ ThereIsAnElection
     /\ EveryoneStaysActiveDuringElection) =>

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?


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.