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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Thu, 7 Feb 2019 12:49:31 -0800 (PST)*References*: <7530440e-0b79-45ee-af76-8a0537a1fd30@googlegroups.com>

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.

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

- 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):