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

[Andrew Helwer]

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