Re: [tlaplus] Re: About "implies" between WF and SF

Awesome.

Yeah. The reason why I sent to our group is: I am not confident enough about my understanding about WF and SF and feel that maybe more EYES can discuss it.

Sometimes, WF and SF relation indeed a bit confusing. I feel it is from the word of "weak" and "strong"

Below is my explanation:

Weak Fairness: Need STRONG condition --ALWAYS ENABLED

Strong Fairness: Need Weak condition. --ONLY infinitely many ENABLED.

Hence, if SF(A) is TRUE, then, surely, WF(A) shall be TRUE.

Then, SF(A)--->WF(A) is TRUE.

On Mon, Jun 7, 2021 at 1:04 PM hwa...@xxxxxxxxx <hwayne@xxxxxxxxx> wrote:

Hi Michael,

Gonna push a fix tonight. Feel free to email me directly about issues like this, I'll see them faster than stuff posted to the newsgroup :)

H

On Monday, 7 June 2021 at 00:42:15 UTC-5 hua...@xxxxxxxxx wrote:
Hillel,

I am reading again your article this evening at https://www.hillelwayne.com/post/fairness/
I feel that the “Weak” fairness implies the existence of “strong” fairness. may introduce bit confusion to beginners.
I mean, the "imply" word could make people get confused. I don't think you want to say:
WF implies SF, which means: WF(A) --> SF(A). However, from TLA+, It should be otherwise. I mean, SF(A)-->WF(A).
I guess you just wanted to tell readers that the "existence of SF". So, maybe we don't want to use "implies" word here, which is more a reserved word for prepositional logic.

Best regards，

Michael

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/nb6uC9v4iV0/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/28ef7079-8f89-46d9-b6b3-250c2e94b9a0n%40googlegroups.com.