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?