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

[tlaplus] Why does liveness checking take so much longer with strong fairness?

I have a simple spec of an eventually-consistent system, the same as in this thread. I run TLC to check this convergence property:

Liveness == converge ~> \A n, o \in Node : state[n] = state[o]

The success of this property requires a fairness assumption on a Gossip action which propagates state from one node to another, as otherwise the system will just stutter indefinitely as a counterexample. If I specify weak fairness for the Gossip action then model checking will complete successfully within five seconds. However, if I specify strong fairness it takes four minutes to complete (also successfully). Why is this? Is this a bug?

Andrew Helwer

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/f4c2b1a1-568f-4ca6-ac63-63e1353241fdn%40googlegroups.com.