CSP semantic model

A representation of a CSP process by specified kinds of observable behaviour. The CSP traces model, CSP stable-failures model and CSP failures-divergences model record progressively more information about refusals and internal activity.

Implementation $I$ has only behaviours permitted by specification $S$ in CSP semantic model $M$. In particular, CSP traces model refinement means $\mathrm{traces}(I)\subseteq \mathrm{traces}(S)$; the other models additionally constrain CSP stable failures or CSP divergences.

Record CSP stable failures and CSP divergences, treating behaviour after a CSP divergence as unrestricted. This can detect both stable refusal of progress and endless internal activity.

Represent a CSP process by its CSP traces and CSP stable failures.

Represent a CSP process by its set of CSP traces.

The possibility, after a finite visible CSP trace, of an infinite sequence of consecutive CSP internal actions. The CSP failures-divergences model records this possibility explicitly.^[ref]

After CSP trace $s$, the CSP process can reach a CSP stable state offering no event in the refusal set $X$. Refusal is existential over reachable stable alternatives.^[ref]

A finite sequence of visible CSP events performed by a CSP process, omitting CSP internal actions.