Hiya,
The two are equivalent, using the following rules:
* P ⋁ ¬Q ≡ Q ⇒ P
* □◇¬P ≡ ¬◇□P
Lamport presents both versions in section 8.4 for Specifying Systems, if you want to read a bit more about that. It comes free with the Toolbox, under the help menu bar.
H
----Folks,
I realized that Hillel Wayne's writing about WF and SF is really awesome for me to understand clearly(hope so) the two concepts.
( https://www.hillelwayne.com/post/fairness/ )
----------------------------------------------------------------------
WF_v(A) == <>[](ENABLED <<A>>_v) => []<><<A>>_v//Weak Fairness: If eventually ALWAYS/KEEP enabled, then will be ALWAYS be EVENTUALLY（Or say, infinitely many) executed.
SF_v(A) == []<>ENABLED <<A>>_v => []<><<A>>_v//Strong Fairness: If NOT NEVER disabled(means could happen sometimes and many times), then will be ALWAYS be EVENTUALLY（Or say, infinitely many) executed.
------------------------------------------------------------
Wayne's explanation is pretty consistent with Lamport's old-tla-src paper(section 3.2) written in 1990.
But, if we read Lamport's 1994 ACM paper, the description was changed by using a more abstracted way as:
//Page 13, ACM Trans on Programming and Systems.weak fairness: ([]<> executed) ∨ ([]<> impossible)
strong fairness: ([]<> executed) ∨ (<>[] impossible)orWFf(A) == ([]<>⟨A⟩f) ∨ ([]<> ¬ Enabled ⟨A⟩f)
SFf(A) == ([]<>⟨A⟩f) ∨ (<>[]¬Enabled ⟨A⟩f)------------------------------------
While I believe Wayne's logic formula for WF and SF is equal to that above in Lamports' 1994 paper, I am wondering why Dr. Lamport changed this part‘上writing from his 1990's paper.
Or should we read Lamport's 1990's TLA paper? What's the difference between the 1990's and the 1994's?
Thanks,
Huailin
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAE7Z%3D%2B5wQ%2BcVxZVk0OuxXaXKu7RPFDA_F_iQafE6qKbipAzJMg%40mail.gmail.com.