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

*From*: Ron Pressler <ron.pressler@xxxxxxxxx>*Date*: Thu, 7 Feb 2019 13:04:36 -0800 (PST)*References*: <7530440e-0b79-45ee-af76-8a0537a1fd30@googlegroups.com> <18b6a2f3-c922-47e9-9aa6-563a458b8371@googlegroups.com>

Would the following translation work?

On Thursday, February 7, 2019 at 9:49:31 PM UTC+1, Leslie Lamport wrote:

-- a: A;b: eitherc1: C1;c2: C2;ord1: D1;d2: D2;end either;e: E;

\* BEGIN TRANSLATION

a == /\ pc = "a"/\ \* translation of A/\ pc' = "b"b == /\ pc = "b"/\ \/ c1\/ c2c1 == /\ 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 ESpec == ... /\ 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 aPlusCal 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.

**Follow-Ups**:**[tlaplus] Re: How does Fairness relate to the State Graph***From:*Ron Pressler

**References**:**How does Fairness relate to the State Graph***From:*david streader

**[tlaplus] Re: How does Fairness relate to the State Graph***From:*Leslie Lamport

- Prev by Date:
**[tlaplus] Re: How does Fairness relate to the State Graph** - Next by Date:
**[tlaplus] Re: How does Fairness relate to the State Graph** - Previous by thread:
**[tlaplus] Re: How does Fairness relate to the State Graph** - Next by thread:
**[tlaplus] Re: How does Fairness relate to the State Graph** - Index(es):