| 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. |