= Solution
Suppose the operands are initially stable and written in <CSP external choice> normal form,
$$
P=\mathop{\square}_{a\in B}a\to P_a,\qquad Q=\mathop{\square}_{a\in C}a\to Q_a.
$$
The <CSP step law> is
$$
\boxed{\begin{aligned}
J_A(P,Q)
&=\mathop{\square}_{a\in B\setminus A}a\to J_A(P_a,Q)\\
&\quad\mathbin\square\mathop{\square}_{a\in C\setminus A}a\to Q_a\\
&\quad\mathbin\square\mathop{\square}_{a\in B\cap C\cap A}a\to J_A(P_a,Q_a).
\end{aligned}}
$$
An empty indexed <CSP external choice> denotes $\mathrm{STOP}$. A label appearing in both of the first two lines must retain both continuations: after that common label the result is the <CSP internal choice> between the continuations. A label in $A$ appears only in the third line and only if both operands offer it. These are exactly the three visible-transition rules from part (d); the two <CSP internal action> rules handle operands that are not initially stable.
As a check, for the paper's example the initial shared $a$ leads to $J_{\{a\}}(b\to\mathrm{STOP},c\to\mathrm{STOP})$. Its expansion is
$$
b\to J_{\{a\}}(\mathrm{STOP},c\to\mathrm{STOP})\mathbin\square c\to\mathrm{STOP}
=b\to c\to\mathrm{STOP}\mathbin\square c\to\mathrm{STOP},
$$
which recovers the displayed example after prefixing by $a$.
Back to article page
