[tlaplus] Re: Why strong fairness implies weak fairness?

[Leslie Lamport <tlaplus.ll@xxxxxxxxx>]

For any properties F, G, and H, if F is stronger than (implies) G, then G => F is stronger than F => H.

Leslie

On Friday, December 27, 2019 at 10:58:40 PM UTC-8, Shiyao MA wrote:

In the pluscal manual, it is stated that,

Strong fairness of (action) A is stronger than (implies) weak fairness of A. In other words, if SFvars (A) is true of a behavior σ, then WFvars (A) is also true of σ. 

Strong fairness is a relaxation of weak fairness as it only requires an action to be *indefinitely* enabled instead of *continuously* enabled, so why will SF(A) => WF(A) ?

Best,

-- 
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/648f7233-5af1-4b5c-a9b6-b5a170ca772b%40googlegroups.com.