As a TLA+ newbie, I found the fairness (weak and strong) formulae in TLA+ a bit hard going initially, so sharing the way I managed to wrap my head around it in case it is of help to others. What I’m hoping to get to is to be able to “read” the formulae in a chunked manner so that they make logical sense to me.

References -

1. Article on stuttering and fairness by Hillel Wayne
2. Caltech course slides (PDF link)
3. The operators of TLA+ by Lamport

I found some of the language used in the Caltech course (pdf link) - easier to retain and recall - particularly the “progress” and “stabilise” operator combinations. These two helped “chunk” some parts of the formulae, making it easier to parse.

Basic notions

$$ \Box{A} = \text{always } A $$

$$ \Diamond{A} = \text{eventually } A $$

$$ \Box{A} = \neg \Diamond \neg A \text{ … i.e. always($A$) means $\neg{A}$ will not eventually occur} $$

$$ \Diamond{A} = \neg \Box \neg A \text{ … i.e. eventually($A$) means $\neg{A}$ will not always be true} $$

.. which yields -

$$ \neg \Box A = \Diamond \neg A $$

.. which is read as “not always A means the same as eventually not A” .. which makes sense.

Defining the notions of “progress” and “stablity”

These are picked from the Caltech course (pdf link) and I found that they read well. In particular, they help chunk combined usages of “always” and “eventually”.

Saying “\(A\) progresses” means \(\neg{A}\) will transition to \(A\) at some time .. or “\(A\) will happen”.

$$ \text{progresses}(A) \overset{\Delta}{=} \text{always}(\text{eventually}(A)) = \Box{\Diamond{A}} $$

Similarly, saying “\(A\) stabilizes” means eventually \(A\) will always be true.

$$ \text{stabilizes}(A) \overset{\Delta}{=} \text{eventually}(\text{always}(A)) = \Diamond{\Box{A}} $$

From the above, we can show that -

$$ \neg\text{stabilizes}(A) = \neg{\Diamond{\Box{A}}} = \neg\neg\Box\neg\Box{A} = \Box\neg\Box{A} = \Box\Diamond\neg{A} = \text{progresses}(\neg{A}) $$

We read that as “A does not stabilize means A will eventually transition to \(\neg{A}\)” … i.e. \(\neg{A}\) will progress. From that, we also see that \(\neg\text{progresses}(A) = \text{stabilizes}(\neg{A})\) .. meaning A does not transition from \(\neg{A}\) to \(A\) means the same as \(\neg{A}\) becoming eventually always true.

Weak and strong fairness

In words, “weak fairness of \(A\)” means insisting that if A becomes continuously enabled at some point, then A will happen. Denoting by \(\langle A \rangle_v\) that “\(A\) happens and results in changes to \(v\)”, the idea of “is enabled” is that the conditions required for \(\langle A \rangle_v\) hold. So \(\text{ENABLED } \langle A \rangle_v\) can be thought of as plucking out of \(\langle A \rangle_v\) those preconditions that have to hold so that the variable changing steps in \(A\) can occur. So the idea of weak fairness translates to -

$$ \text{WF}_v(A) = \text{stabilizes}(\text{ ENABLED } \langle A \rangle_v) \Rightarrow \text{progresses}(\langle A \rangle_v) $$ $$ = \Diamond{\Box{\text{ ENABLED } \langle A \rangle_v}} \Rightarrow \Box{\Diamond{\langle A \rangle_v}} $$

And “strong fairness of \(A\)” means insisting that if \(A\) becomes enabled at some point, then A will happen. As the name implies, this is a stronger condition since it doesn’t require \(A\) to become continuously enabled and it can keep switching between enabled and not enabled.

$$ \text{SF}_v(A) = \text{progresses}(\text{ ENABLED } \langle A \rangle_v) \Rightarrow \text{progresses}(\langle A \rangle_v) $$ $$ = \Box{\Diamond{\text{ ENABLED } \langle A \rangle_v}} \Rightarrow \Box{\Diamond{\langle A \rangle_v}} $$

These two forms are as described in Hillel Wayne’s article, but they’re first stated and explained there instead of being derived from smaller concepts such as “stabilizes” and “progresses”.

Also, since \(A \Rightarrow B\) is the same as \(\neg{A} \bigvee B\), \(\text{WF}_v(A)\) can also be rewritten as -

$$ \text{WF}_v(A) = \neg\text{stabilizes}(\text{ ENABLED } \langle A \rangle_v) \bigvee \text{progresses}(\langle A \rangle_v) $$ $$ = \text{progresses}(\neg\text{ ENABLED } \langle A \rangle_v) \bigvee \text{progresses}(\langle A \rangle_v) $$ $$ = \Box{\Diamond{\neg\text{ ENABLED } \langle A \rangle_v}} \bigvee \Box{\Diamond{\langle A \rangle_v}} $$

… and similarly, we can express \(\text{SF}_v(A)\) as

$$ \text{SF}_v(A) = \neg\text{progresses}(\text{ ENABLED } \langle A \rangle_v) \bigvee \text{progresses}(\langle A \rangle_v) $$ $$ = \text{stabilizes}(\neg\text{ ENABLED } \langle A \rangle_v) \bigvee \text{progresses}(\langle A \rangle_v) $$ $$ = \Diamond{\Box{\neg\text{ ENABLED } \langle A \rangle_v}} \bigvee \Box{\Diamond{\langle A \rangle_v}} $$

These two formula above are as given in The operators of TLA+ paper (pdf link) by Leslie Lamport.

So the above work covers both Hillel’s explanation as well as Lamport’s expression. I’m now somewhat satisfied.