[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?
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.