  Hoare's Communicating Sequential Processes (CSP) admits a rich universe of
semantic models closely related to the van Glabbeek spectrum. In this paper we
study finite observational models, of which at least six have been identified
for CSP, namely traces, stable failures, revivals, acceptances, refusal testing
and finite linear observations. We show how to use the recently-introduced
\emph{priority} operator to transform refinement questions in these models into
trace refinement (language inclusion) tests. Furthermore, we are able to
generalise this to any (rational) finite observational model. As well as being
of theoretical interest, this is of practical significance since the
state-of-the-art refinement checking tool FDR4 currently only supports two such
models. In particular we study how it is possible to check refinement in a
discrete version of the Timed Failures model that supports Timed CSP.
