[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: How does Fairness relate to the State Graph
Obviously, the `either` is not allowed to share a label with a loop.
On Thursday, February 7, 2019 at 11:32:55 PM UTC+1, Ron Pressler wrote:
Right. A more straightforward translation might be:
b__BRANCH1 == pc = "b" /\ pc' = "c1"
b__BRANCH2 == pc = "b" /\ pc' = "d1"
/\ ... \* translation of C1
/\ ... \* translation of C2
Spec == ... /\ WF_vars(b) /\ WF_vars(b__BRANCH1) /\ WF_vars(b__BRANCH2) /\ ...
So the two branch definitions are always generated. Their kind of fairness is determined by that of whatever label the `either` is in.
This only slightly increases the complexity of the current translation; whether this is more or less intuitive is not for me to say.
On Thursday, February 7, 2019 at 11:18:40 PM UTC+1, Leslie Lamport wrote:
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.