= Solution
Write $J_A(P,Q)=P\mathbin\triangle_AQ$. The following five <CSP operational semantics> rules suffice, with $a$ always visible:
$$
\frac{P\xrightarrow{\tau}P'}{J_A(P,Q)\xrightarrow{\tau}J_A(P',Q)}\qquad
\frac{Q\xrightarrow{\tau}Q'}{J_A(P,Q)\xrightarrow{\tau}J_A(P,Q')},
$$
$$
\frac{P\xrightarrow aP'\quad a\notin A}{J_A(P,Q)\xrightarrow aJ_A(P',Q)}\qquad
\frac{Q\xrightarrow aQ'\quad a\notin A}{J_A(P,Q)\xrightarrow aQ'},
$$
$$
\boxed{\frac{P\xrightarrow aP'\quad Q\xrightarrow aQ'\quad a\in A}{J_A(P,Q)\xrightarrow aJ_A(P',Q')}.}
$$
Thus a <CSP internal action> of either operand preserves the wrapper. A visible action outside $A$ by the left operand also preserves it, whereas such an action by the right operand performs an ordinary <CSP interrupt> and discards the left operand. An action in $A$ requires both operands and advances both without discarding either. If both can perform the same event outside $A$, there are two transitions with the same visible label and potentially different derivatives; neither should be deleted. The paper excludes successful termination, so no extra termination rules are needed.
Back to article page
