[tlaplus] Meaning of conjunction or disjunction of fairness

[Jones Martins <jonesmvc@xxxxxxxxx>]

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.