Meaning of conjunction or disjunction of fairness

[Jones Martins]

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

   

[Stephan Merz]

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/02911f5c-fbab-4792-ac86-f0e48100924en%40googlegroups.com.

[Jones Martins]

Thank you, Stephan

That's all I needed! I'm worried about writing specifications with realistic fairness. For example, I can't simply apply Strong Fairness to all actions.

Jones

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/MLdB9oKjRtE/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/032EE056-98C3-4217-930C-8A3DF8C90C5E%40gmail.com.