[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;
   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.