Re: [tlaplus] About WF and SF operators' semantics

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

On Sun, Apr 25, 2021 at 5:48 PM Hillel Wayne <hwayne@xxxxxxxxx> wrote:

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

On 4/25/2021 5:51 PM, Huailin wrote:

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

--
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.

--
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/23929355-f9fe-f4d6-3bab-a32424b2f1e5%40gmail.com.