# [tlaplus] Re: How does Fairness relate to the State Graph

Sorry, I meant:

b == /\ pc = "b"
/\ \/ c1
\/ d1

On Thursday, February 7, 2019 at 10:04:36 PM UTC+1, Ron Pressler wrote:
Would the following translation work?

a: A;
b: either
c1:   C1;
c2:   C2;
or
d1:  D1;
d2:  D2;
end either;
e: E;

\* BEGIN TRANSLATION

a == /\ pc = "a"
/\ \* translation of A
/\ pc' = "b"

b == /\ pc = "b"
/\ \/ c1
\/ c2

c1 == /\ pc = "b" \* <----- no "c1" pc
/\ ... \* translation of C1
/\ pc' = "c2"

c2 == /\ pc = "c2"
/\ ... \* translation of C2
/\ pc' = "e"

d1 == /\ pc = "b" \* <----- no "d1" pc
/\ ... \* translation of D1
/\ pc' = "d2"

d2 == /\ pc = "d2"
/\ ... \* translation of D2
/\ pc' = "e"

e == /\ pc = "e"
/\ ... \* translation of E

Spec == ... /\ WF_vars(c1) /\ WF_vars(d1) /\ ...

On Thursday, February 7, 2019 at 9:49:31 PM UTC+1, Leslie Lamport wrote:
if the translation made the branch occur between different steps

The translation doesn't make anything happen.  The translation maps a
PlusCal algorithm to a TLA+ formula.  If you can explain what TLA+ formula
you would like the either...or statement to be mapped to, we can discuss
whether that would be a good translation.

But all of this is only relevant if other peoples intuition is that a
fair execution of the small program would indeed terminate.

People's intuition about concepts they don't understand is irrelevant.
I have no trouble accepting that the earth is moving me at over 1000 km
per hour as I type this, even though it contradicts people's intuition.

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.