[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

Would the following translation work?

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

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.