b == /\ pc = "b"/\ \/ c1\/ d1
Would the following translation work?a: A;b: eitherc1: C1;c2: C2;ord1: D1;d2: D2;end either;e: E;\* BEGIN TRANSLATIONa == /\ 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.