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

I don't think that works for three reasons:

1. You can also write PlusCal specs like

B: either x := 1; c1: x := 2; c2: x := 3; or x := 4; d1: x := 5; d2: x := 6;

In which case inlining c1 would make it impossible, as you'd have x' = 1 /\ x' = 2.

2. I may not want b and c1 to both be true in the same next-step relation, f.ex if I'm modeling a concurrent system that has a delay between picking a choice and actually making it.

3. One of the things I think is important about PlusCal is that it's conceptually simple: PlusCal labels map in a fairly straightforward way onto TLA+ actions, and the translator doesn't try to guess your intentions. If we inline labels then we break that assumption. You might misunderstand what a spec does not because of spec syntax but because of how it is translated.

My personal preference is to keep PlusCal small and make it clear when learners hit the limits of what's easily expressible in it.

On 2/7/19 3:21 PM, Ron Pressler wrote:

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.

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