Read on Twitter
OK, here& #39;s why I found weak fairness confusing, a thread that nobody will care about except possibly @hillelogram https://twitter.com/hillelogram/status/1279103160045404161">https://twitter.com/hillelogr...
I& #39;ll probably get something technically incorrect in this thread (probably mixing steps and actions), in which case @pressron will undoubtedly correct me
Here& #39;s the definition of weak fairness, as shown in the appendix of Hillel& #39;s post:
WF_v(A) == ⃟ ⃞(ENABLED 〈A〉_v) => ⃞ ⃟〈A〉_v
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!)
(Not all specs have this property, but if your A is a sub-action of Next, then many do!)
To formalize the above, I& #39;m talking about specs where the following holds:
〈A〉_v => ~ (ENABLED 〈A〉_v)& #39;
After an A step, action A is no longer enabled.
〈A〉_v => ~ (ENABLED 〈A〉_v)& #39;
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!
⃟ ⃞(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& #39;s more complex:
(〈A〉_v => ~ (ENABLED 〈A〉_v)& #39;) =>
~ ⃟ ⃞(ENABLED 〈A〉_v
This says, if an A step means that A will no longer be enabled, then A can& #39;t eventually be enabled forever.
(〈A〉_v => ~ (ENABLED 〈A〉_v)& #39;) =>
~ ⃟ ⃞(ENABLED 〈A〉_v
This says, if an A step means that A will no longer be enabled, then A can& #39;t eventually be enabled forever.
Now, I realize that it& #39;s not true in general that:
〈A〉_v => ~ (ENABLED 〈A〉_v)& #39;
(In fact, if you choose "Next" as the action, then if it was true you& #39;d have deadlock!).
〈A〉_v => ~ (ENABLED 〈A〉_v)& #39;
(In fact, if you choose "Next" as the action, then if it was true you& #39;d have deadlock!).
Anyways, that has been the source of my struggles on understanding the definition of weak fairness.
fin
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& #39;re just weird overlapping shapes.
