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

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

   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.