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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Thu, 2 Jan 2020 09:51:47 -0800 (PST)*References*: <f675b9ad-4136-46ae-a3f7-4f294c3c3816@googlegroups.com>

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:

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.

**Follow-Ups**:**Re: [tlaplus] Re: Why strong fairness implies weak fairness?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Updating a variable inside a filtering condition (like CHOOSE ) causes TLC exception.** - Next by Date:
**Re: [tlaplus] Re: Why strong fairness implies weak fairness?** - Previous by thread:
**Re: [tlaplus] Updating a variable inside a filtering condition (like CHOOSE ) causes TLC exception.** - Next by thread:
**Re: [tlaplus] Re: Why strong fairness implies weak fairness?** - Index(es):