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

[Ron Pressler <ron.pressler@xxxxxxxxx>]

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.