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

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

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


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) ?


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.