[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# [tlaplus] About WF and SF operators' semantics

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.