= Solution
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 compare
$$
G=a\to\mathrm{STOP},\qquad B=\bigl(a\to\mathrm{STOP}\mathbin\square h\to a\to\mathrm{STOP}\bigr)\setminus\{h\}.
$$
In $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> $\langle\rangle$ and $\langle a\rangle$. Initially their possible stable observations offer exactly $a$, so their initial <CSP stable failures> are precisely $(\langle\rangle,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. Therefore
$$
\boxed{G=_T B,\quad G=_F B,\quad G=_{FD}B,\qquad\text{but the property separates }G\text{ and }B.}
$$
No <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.
Back to article page
