Erratum

The relational definition of weak refinement, Definition 11.2.1 on page 258, is too strong - both in terms of the subsequent definitions and in terms of what is desirable. The correct definition would have

$$\bigcup \hat{p}_C \subseteq \bigcup \hat{p}_A$$

in place of the quantifications over $\hat{p}_C$ and $\hat{p}_A$. A counterexample is a system with 1 visible operation and one internal one. The abstract internal operation relates the initial state 0 to $1$ and $1$ to $2$, and in the concrete system relates 0 (initial) to $1$ or $2$. The visible operation outputs the state in either system. This satisfies our subsequent definitions of weak refinement, and would be seen as a refinement (the difference between 1 or 2 internal operations taking place cannot be observable), but does not satisfy Definition 11.2.1.