Re: [tlaplus] Science of Concurrent Programs: 3.4.1.4 Error in Composition?

---- MODULE ActionComposition ----
EXTENDS Naturals
CONSTANTS Procs, NumberDone

VARIABLES x, t, pc
vars == << x, t, pc >>

Init ==
/\ x = 0
/\ t = [ p \in Procs |-> 0 ]
/\ pc = [ p \in Procs |-> "a" ]

aStep(p) ==
/\ pc[p] = "a"
/\ x' = x
/\ t' = [ t EXCEPT ![p] = x ]
/\ pc' = [ pc EXCEPT ![p] = "b" ]

bStep(p) ==
/\ pc[p] = "b"
/\ x' = t[p] + 1
\*/\ x' = t'[p] + 1 \*Suggested errata is causing error
/\ t' = t
/\ pc' = [ pc EXCEPT ![p] = "done" ]

aStep_bStep(p) ==
/\ pc[p] = "a"
\*/\ x' = t[p] + 1
\*/\ x' = t'[p] + 1 \*Causing error if before the next line
/\ t' = [t EXCEPT ![p] = x]
/\ x' = t'[p] + 1 \*Passing if you put this here
/\ pc' = [pc EXCEPT ![p] = "done"]

PgmStep == \E p \in Procs:
\*\/ aStep(p)
\*\/ bStep(p)
\/ aStep_bStep(p) \*Alternative action composition

Stutter ==
/\ \A p \in Procs: pc[p] = "done"
\*/\ <<x',t',pc'>> = << x, t, pc >> \*does not work
\*/\ vars' = vars \*does not work
/\ UNCHANGED vars \*This works

Next == PgmStep \/ Stutter

TypeOK ==
/\ x \in Nat
/\ t \in [Procs -> Nat]
/\ pc \in [Procs -> {"a", "b", "done"}]

Inv ==
/\ TypeOK
/\ \A p \in Procs: (pc[p] = "b" => (t[p] =< NumberDone))
/\ x =< NumberDone

Composition ==
/\ TRUE
\*/\ [][\A p \in Procs: aStep(p) \cdot bStep(p) => pc[p] = "done"]_vars
\*/\ [][\A p \in Procs: aStep_bStep(p) => pc[p] = "done"]_vars
\*/\ [][\A p \in Procs: aStep(p) \cdot bStep(p) => aStep_bStep(p)]_vars
\*/\ [][\A p \in Procs: aStep_bStep(p) => aStep(p) \cdot bStep(p)]_vars

On Monday, November 24, 2025 at 2:44:03 PM UTC-8 Dave Hughes wrote:

If someone is updating this work then two other lesser things might want to be fixed:

on page 50 the reference to the definition of except is incorrectly cited as 2.8.2 - it is actually introduced at he top of page 47 in 3.3 introduction.

The abstract program in fig. 3.5 on page 54 is missing the definition of TypeOk and NumberDone, which may be cut and pasted from page 51.

Dave

From: tla...@xxxxxxxxxxxxxxxx <tla...@xxxxxxxxxxxxxxxx> on behalf of Andrew Helwer <andrew...@xxxxxxxxx>
Sent: Monday, November 24, 2025 20:49

To: tla...@xxxxxxxxxxxxxxxx <tla...@xxxxxxxxxxxxxxxx>
Subject: Re: [tlaplus] Science of Concurrent Programs: 3.4.1.4 Error in Composition?

Your programmer's intuition isn't wholly misplaced. If you were to write an interpreter for this action, you would have to identify that the value of x' relies on the value of t' and thus you have to evaluate t' before x', even though your interpreter encounters x' in the conjunction list first. Of course this is getting away from Lamport's intended perspective that you view actions as predicates on pairs of states pulled out of the mathematical ether, but when we want to check this on actually existing physical computers we have some practical constraints. I've found that a lot of TLA+ familiarity requires smoothly shifting between these different perspectives depending on the context.

Andrew

On Mon, Nov 24, 2025 at 11:39 AM Dave Hughes <dbah...@xxxxxxxxx> wrote:

Thanks for your comprehensive responses - they helped me understand better - i think Lamport's intended solution was the t'(p)+1 because that makes the footnote 5 make sense! Until I saw this i could not understand the point of the footnote. As a programmer it is uncomfortable - and just removing the 3^rd conjunct is easier (for me) - but that is not what he is trying to show - I think.

Dave

From: tla...@xxxxxxxxxxxxxxxx <tla...@xxxxxxxxxxxxxxxx> on behalf of Stephan Merz <stepha...@xxxxxxxxx>
Sent: Monday, November 24, 2025 20:22
To: tla...@xxxxxxxxxxxxxxxx <tla...@xxxxxxxxxxxxxxxx>
Subject: Re: [tlaplus] Science of Concurrent Programs: 3.4.1.4 Error in Composition?

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 <dbah...@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+u...@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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/3F39D6C4-274D-4369-A0EB-7B78A4389C04%40gmail.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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/MN2PR12MB318446FF96AE120E1B960D72F2D0A%40MN2PR12MB3184.namprd12.prod.outlook.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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUUCbzt-ffxoYGfeu%3DTiQdDLQ0D9Wt5114LTaMy0Lj5vxA%40mail.gmail.com.