About WF and SF operators' semantics

[Huailin]

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)

or

WFf(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

[Hillel Wayne]

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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAE7Z%3D%2B5wQ%2BcVxZVk0OuxXaXKu7RPFDA_F_iQafE6qKbipAzJMg%40mail.gmail.com.

[Huailin]

yeah. but i feel your writing is really good. thanks huge. I have been confusing with the WF and SF until reading your blogs.

BTW, are there any TLA fans in silicon valley, besides Dr. Lamport? 

Really like to, after the COVID-19 lock-down, have some regular meetups and have a drink or milk team. It would be wonderful if I can treat Dr. Lamport a milk tea, which is so popular these days in silicon valley.

Huailin

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/23929355-f9fe-f4d6-3bab-a32424b2f1e5%40gmail.com.