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
Hello, everyone
I was wondering what does each option say about our system (or if it's incorrect).
\A v \in Values:
\/ WF_Vars(AtoB(v))
\/ WF_Vars(BtoC(v))
\E v \in Values:
\/ WF_Vars(AtoB(v))
\/ WF_Vars(BtoC(v))
\A v \in Values:
/\ WF_Vars(AtoB(v))
/\ WF_Vars(BtoC(v))
\E v \in Values:
\/ WF_Vars(AtoB(v))
\/ WF_Vars(BtoC(v))
Regards,
Jones
--
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/02911f5c-fbab-4792-ac86-f0e48100924en%40googlegroups.com.