| You are correct to point out that this definition is wrong. Logically, action composition of two actions A(x, x’) and B(x,x’) where x denotes a tuple of all state variables corresponds to the conjunction \E x’’ : A(x, x’’) /\ B(x’’, x’) where x’’ is a fresh tuple of variables. In the example we get
aStep(p) . bStep(p) = \E x’’, t’’, pc’' : /\ pc(p) = a /\ x’’ = x /\ t’’ = (t EXCEPT p |-> x) /\ pc’’ = (pc EXCEPT p |-> b) /\ pc’’(p) = b /\ x’ = t’’(p) + 1 /\ t’ = t’' /\ pc’ = (pc’’ EXCEPT p |-> done)
Some simplification, in particular using the "one-point rule" (\E y : y = t /\ A(y)) = A(t), yields
aStep(p) . bStep(p) = /\ pc(p) = a /\ x’ = x+1 \* alternatively: x’ = t’(p)+1 /\ t’ = (t EXCEPT p |-> x) /\ pc’ = (pc EXCEPT p |-> done)
Stephan On 24 Nov 2025, at 18:34, Dave Hughes <dbahughes@xxxxxxxxx> wrote:
The composition of steps a and b from figure 3.5 is listed in 3.4.1.4 on page 58 as:
aStep(p). bStep(p) = /\ pc(p) = a /\ x’ = t(p)
+ 1 /\ t’ = (t EXCEPT
p |-> x ) /\ pc’ = (pc EXCEPT p |-> done) This to me seems wrong since t is only changed when that process is about to be set to done and hence is never accessed. So as far as i can see this will only ever set x' to one of the initial values of t (+1) - so will always end at one since t is initialized to zero for all processes. I am fairly new to TLA and a little terrified to question this so i apologize in advance if i am wasting peoples time - but all my efforts to make sense of this have failed. In some ways this is a bit of a weird example since the temporary variable was introduced to illustrate issues of concurrency - and when you compose the steps it becomes irrelevant- naturally. Thanks for any help! Dave Hughes
--
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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/c36ba172-2f6e-40e8-9ec3-5f47db63ddd9n%40googlegroups.com.
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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/3F39D6C4-274D-4369-A0EB-7B78A4389C04%40gmail.com.
|