OK, here's why I found weak fairness confusing, a thread that nobody will care about except possibly @hillelogram https://twitter.com/hillelogram/status/1279103160045404161

I'll probably get something technically incorrect in this thread (probably mixing steps and actions), in which case @pressron will undoubtedly correct me

Here's the definition of weak fairness, as shown in the appendix of Hillel's post:

WF_v(A) == ⃟ ⃞(ENABLED 〈A〉_v) => ⃞ ⃟〈A〉_v

The confusion in my mind arises when looking at a spec where, if an action A is enabled in a state, and then there is an A step, then A is not enabled in the next state.

(Not all specs have this property, but if your A is a sub-action of Next, then many do!)

To formalize the above, I'm talking about specs where the following holds:

〈A〉_v => ~ (ENABLED 〈A〉_v)'

After an A step, action A is no longer enabled.

So, substituting that into weak fairness:

⃟ ⃞(ENABLED 〈A〉_v) => ⃞ ⃟~ (ENABLED 〈A〉_v)

Or, if we LET X == ENABLED 〈A〉_v:

⃟ ⃞ X => ⃟~X

That statement (if X is eventually always true, then X is eventually not true) is *super* confusing!

This makes more sense to me, even though it's more complex:

(〈A〉_v => ~ (ENABLED 〈A〉_v)') =>
~ ⃟ ⃞(ENABLED 〈A〉_v

This says, if an A step means that A will no longer be enabled, then A can't eventually be enabled forever.

Now, I realize that it's not true in general that:

〈A〉_v => ~ (ENABLED 〈A〉_v)'

(In fact, if you choose "Next" as the action, then if it was true you'd have deadlock!).

Anyways, that has been the source of my struggles on understanding the definition of weak fairness.

fin

Postscript: trying to use unicode characters for box and diamond was a mistake. The diamond renders as a box in Chrome, and in Safari they're just weird overlapping shapes.