Why strong fairness implies weak fairness?

[Shiyao MA]

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,

[Leslie Lamport]

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

Leslie

[Stephan Merz]

That should certainly be: if F is stronger than (implies) G, then G => H is stronger than F => H.

Stephan

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