universal quantification is stronger than existential quantification (assuming Values is non-empty) and conjunction is stronger than disjunction. For example,
\A v \in Values:
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.
\E v \in Values:
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.
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.