Let's consider a simpler version first: say we have two processes one of which increments x and the other y.
A non-interleaving specification that allows both processes to execute simultaneously can be written as
NextXY_NI ==
\/ X /\ [Y]_y
\/ Y /\ [X]_x
Now let's consider the case where the two processes update a shared variable, similar to your original example
XZ == x' = x+1 /\ z' = z+1
YZ == y' = y+1 /\ z' = z-1
The interleaving specification will be similar to the one above:
NextXYZ_IL ==
\/ XZ /\ y' = y
\/ YZ /\ x' = x
What should the non-interleaving specification be? I don't think there is a unique answer because it is not clear how to reconcile the conflicting updates to the shared variable z. One possible choice would be
NextXYZ_NI ==
\/ (XZ /\ y' = y) \cdot [YZ /\ x' = x]_<<x,y,z>>
\/ (YZ /\ x' = x) \cdot [XZ /\ y' = y]_<<x,y,z>>
where \cdot is the action composition operator. In other words, the two actions may be performed in a single atomic step, in either order. Expanding the definitions of the actions and of \cdot (which isn't handled by TLC) in the first disjunct, we obtain
\E x'',y'',z'' :
/\ x'' = x+1 /\ z'' = z+1 /\ y'' = y
/\ \/ y' = y''+1 /\ z' = z''-1 /\ x' = x''
\/ x' = x'' /\ y' = y'' /\ z' = z''
which can be simplified to
/\ x' = x+1
/\ \/ y' = y /\ z' = z+1
\/ y' = y+1 /\ z' = z \* actually, z' = (z+1)-1
The result for the second disjunct is similar.
Note that the formula NextXY_NI above is equivalent to
\/ (X /\ y' = y) \cdot [Y /\ x'=x]_<<x,y>>
\/ (Y /\ x' = x) \cdot [X /\ y'=y]_<<x,y>>
so it appears that the above definition is systematic. But again, I think it is only one possible choice of what one means by non-interleaving composition. If I correctly understand your definition, you let one of the processes update the shared variable and ignore the update coming from the other process.
Stephan