Hi,
I've found a fairness requirement that works in this case, shown below.
But first, worth mentioning that TLC is right: according to the specification, it's not clear that the actors will ever converge.
For example, maybe in practice one actor moves to PREPARE state at 3 PM once per day, waits 1 hour, and if no other actor is in PREPARE state, goes back to IDLE.
The other actor moves to PREPARE state at 10 PM and waits for 1 hour. They'll never align.
But, if you can convince yourself that in your system that's not the case, then for two actors we need another strong fairness requirement, informally:
(i) If one actor is in the PRAPRE state infinitely often, then the other actor will move to the PREPARE state as well. After that, your strong fairness requirement (3) will take place.
For three actors, we need two strong fairness conditions:
(ii) If two actors are in the PREPARE state infinitely often, then the third actor will move to that state as well, combined with condition (i).
For four actors we will need already three strong fairness conditions.
What's happening here is that one actor is periodically in the PREPARE state, but there's a requirement that if that happens then another actor will move to that state.
Now two actors are periodically in the PREPARE state, and there's a requirement that if that happens then another actor will move to that state.
And so on and so forth.
In the link, ConvergingLivenessCondition.tla is the spec itself.
In it, you'll find the basic spec, for any number of actors; An example of a strong requirement for two actors; Another example for three actors; A generalization that doesn't work because of Java StackOverflowError exception due to usage of recursive definition that has SF_vars in it (to make it similar to the specific cases of two and three actors); And a workaround without recursion of any number of actors.
Also, you can find there MC files for two actors, three actors, three actors but with a generalized approach but manually written, and six actors with a generalized approach that will work for any number of actors without having to manually write that.
Note that it's heavy. Running it for six actors took me 12 seconds, and I wasn't able to complete it for ten actors because I ran out of memory (which can be adjusted via the configuration).
Here's the generalized approach:
ChooseActorNotInPrepare(actors) == CHOOSE self \in actors: pc[self] # "PREPARE"
ChooseActorInPrepare(actors) == CHOOSE self \in actors: pc[self] = "PREPARE"
ConvergingGeneralAction == pc' = [pc EXCEPT ![ChooseActorNotInPrepare(ProcSet)] = "PREPARE"]
RECURSIVE InPrepareState(_,_)
InPrepareState(n, actors) == IF n = 0 THEN TRUE
ELSE /\ n > 0
/\ actors # {}
/\ \E selfPrepared \in actors: pc[selfPrepared] = "PREPARE"
/\ InPrepareState(n-1, actors \ { ChooseActorInPrepare(actors) })
ConvergingConditionForNActors(n) ==
/\ InPrepareState(n, ProcSet)
/\ \E selfNotPrepare \in ProcSet: pc[selfNotPrepare] # "PREPARE"
ConvergingSpec == /\ Spec
/\ \A i \in 1..(NumOfActors-1): SF_vars(ConvergingConditionForNActors(i) /\ ConvergingGeneralAction)
THEOREM ConvergingSpec => EventuallyDone
Hope it helps,
Samyon.