Past exam of the computer science course of the University of Oxford / 2015 / Concurrency / 1 / e

The obstruction is that the property is about where a transition originates, whereas the three standard CSP semantic models identify processes that can disagree about this fact. Take fresh $h\ne a$ and compareIn $G$, the only $a$ transition leaves a CSP stable state, so the property holds. Initially $B$ has both an $a$ transition to $\mathrm{STOP}$ and a CSP internal action to $a\to \mathrm{STOP}$. Its initial state is therefore not a CSP stable state, and its direct $a$ transition violates the property.

Nevertheless both have exactly the CSP traces $⟨⟩$ and $⟨a⟩$. Initially their possible stable observations offer exactly $a$, so their initial CSP stable failures are precisely $(⟨⟩,X)$ with $a\notin X$. After $a$, both can refuse every CSP event. Neither has a CSP divergence: the hidden $h$ can occur at most once. ThereforeNo CSP refinement test in one of these models can separate semantically equal operands. This also rules out placing the operand in a fixed context of ordinary CSP operators before the test, since those operators respect the model's equality. A model recording more about the interleaving of stability and acceptance, or an additional operator that explicitly observes stability, would be needed.