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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 22 Dec 2021 10:28:36 +0100*References*: <02911f5c-fbab-4792-ac86-f0e48100924en@googlegroups.com>

Hello, universal quantification is stronger than existential quantification (assuming Values is non-empty) and conjunction is stronger than disjunction. For example, \A v \in Values: /\ WF_Vars(AtoB(v)) /\ WF_Vars(BtoC(v)) says that both transitions AtoB and BtoC must eventually occur when they remain enabled, for every possible value. This is typically what you want : any value that is at "A" will eventually move to "B" and then to "C", assuming that there are no conflicting transitions. In contrast, \E v \in Values: \/ WF_Vars(AtoB(v)) \/ WF_Vars(BtoC(v)) is a very weak condition. Assuming that at least one value v is initially at "A", a behavior that stutters forever satisfies this fairness condition: v is never at "B", thus the transition BtoC is always disabled for value v, and therefore the fairness condition WF_Vars(BtoC(v)) holds, hence the entire formula. Figuring out the meaning of the other conditions is a nice exercise. Regards, 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/032EE056-98C3-4217-930C-8A3DF8C90C5E%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Meaning of conjunction or disjunction of fairness***From:*Jones Martins

**References**:**[tlaplus] Meaning of conjunction or disjunction of fairness***From:*Jones Martins

- Prev by Date:
**[tlaplus] Verifying concurrent data structures** - Next by Date:
**Re: [tlaplus] Meaning of conjunction or disjunction of fairness** - Previous by thread:
**[tlaplus] Meaning of conjunction or disjunction of fairness** - Next by thread:
**Re: [tlaplus] Meaning of conjunction or disjunction of fairness** - Index(es):