= Solution
Let $X=P\ {}_{\{a,b,d\}}\Vert_{\{a,b,c\}}\ Q$. In this <CSP alphabetized parallel composition>, $a,b$ require both participants, $d$ belongs only to the left participant and $c$ only to the right participant. Expand the reachable states using <CSP prefixing> and <CSP external choice>:
$$
\begin{aligned}
X&=a\to Y,\\
Y&=b\to Z\mathbin\square d\to W,\\
W&=b\to Z,\\
Z&=c\to X.
\end{aligned}
$$
For example, after the synchronized $b$, the left participant is back at $P$ but the right participant is at $c\to Q$. The left participant's proposed $a$ is blocked until the right participant has performed $c$. Similarly, after $a,d$, only the synchronized $b$ is possible. Thus there is no extra interleaving to include.
Eliminating $Y,W,Z$ gives the guarded equation
$$
X=a\to\bigl(b\to c\to X\mathbin\square d\to b\to c\to X\bigr).
$$
Consequently choose the sequential <CSP process>
$$
\boxed{R=a\to\bigl(b\to c\to R\mathbin\square d\to b\to c\to R\bigr).}
$$
The <unique fixed point principle> first establishes $R=X$.
Now let $E=X\mathbin\Theta_{\{c\}}X$. The <CSP exception> operator follows its left operand until that operand performs $c$, includes this $c$ in the visible behaviour, and then switches to its right operand. Applying its <CSP step law> to the four-state expansion yields
$$
E=a\to\bigl(b\to c\to X\mathbin\square d\to b\to c\to X\bigr)=X.
$$
The switch occurs exactly where the ordinary execution already returns to $X$. Therefore $E=X=R$. The answer uses neither a <CSP exception> operator nor a <CSP parallel composition> operator, and the argument gives equality in all three standard <CSP semantic models>.
Back to article page
