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

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

I don't understand Hillel's point 1, since I assumed the proposed
translation would apply only when there is no code between label b and
label c1 or d1.  His point 2 isn't compelling either, because the
difference between control in process p being at b or at c1 or at c2
is observable only by reading value of pc[p], and in multiprocess
algorithms, other processes are usually assumed not to be able to
access that value.

However, the proposal is unacceptable because it would provide a
quite unexpected translation if C1 or D1 were a while loop.


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.