Strong fairness means an action which is enabled infinitely often will eventually be taken. So it can be disabled and renabled over and over, but as long as it always gets renabled, then it will eventually be taken. Which is essentially what you said.
But if, for example, an action is enabled infinitely often and there are _two_ ways to step out of it (because of non determinism in the action), you are NOT guaranteed that both ways out will eventually be taken.
To guarantee that, you’d have to further subdivide the action, and have strong fairness on the subdivisions.
As an example,
Foo == /\ x = 1
/\ \E y \in {2, 3} : x’ = y
If x is repeatedly toggled between 0 and 1 by some other action, and you have strong fairness on Foo, then you’re guaranteed that the Foo action will eventually take place. But it taking place by always choosing 2 would be valid, there’s no guarantee that eventually it would assign 3 to x in the next state.
My guess is that your PlusCal is being turned into actions which contain non-determinism, and TLC is showing you a trace where only one side of the non-determinism ever occurs.
I hope this helps!
Jay P.
Attachment:
hackStateGraph.png
Description: PNG image
Attachment:
abpHack.tla
Description: Binary data
