[tlaplus] What to do when strong fairness isn't strong enough?

Occasionally when I set out to specify liveness properties I'll run into a problem like this:

A number of actors each want to transition from IDLE to PREPARED, and then from PREPARED to DONE. Once an actor is DONE they stay DONE, but they can go backwards from PREPARED to IDLE if the situation looks dicey.

IDLE <---> PREPARED ---> DONE

The actors follow these rules:

It is always safe to go from IDLE to PREPARED
It is always safe to revert from PREPARED to IDLE
It is only safe to go from PREPARED to DONE if every actor is PREPARED. Fortunately, the actors can atomically read each other's state and modify their own, so there's no "Two Generals" problem here.

I'm willing to assume strong fairness on (1) and (3).

Amazingly (to me), this turns out not to be enough to ensure that any actor reaches the DONE state. TLC discovers a very clever loop in the attached two-actor spec:

Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
/\ BobState = "IDLE"
/\ AliceState = "IDLE"

State 2: <AlicePrepare line 14, col 5 to line 16, col 25 of module NervousActors>
/\ BobState = "IDLE"
/\ AliceState = "PREPARED"

State 3: <AliceRevert line 19, col 5 to line 21, col 25 of module NervousActors>
/\ BobState = "IDLE"
/\ AliceState = "IDLE"

State 4: <BobPrepare line 24, col 5 to line 26, col 27 of module NervousActors>
/\ BobState = "PREPARED"
/\ AliceState = "IDLE"

Back to state 1: <BobRevert line 29, col 5 to line 31, col 27 of module NervousActors>

Sure enough, in that trace it is true that Alice always eventually prepares and Bob always eventually prepares, but they get very unlucky and never manage to be prepared at the same time.

I don't think there's a fairness criteria I can add to make the liveness property hold. What is an elegant way to express the (vague, informal) requirement that "Alice and Bob never stay misaligned forever"?

I have a few ideas, but none that generalize cleanly to systems with more than two actors or to algorithms with more than two steps per actor.

Calvin