= CSP refusal set
{c}
A <CSP refusal set> is a set $X$ of visible <CSP events> that a process can decline together in a stable <state>. Stability excludes an enabled internal transition. Pairing $X$ with a preceding trace gives a failure observation; different internal resolutions after the same trace can produce different <CSP refusal sets>[refusal sets].<The CSP View of the World in the FDR2 User Manual>[§1.2, stable failures definition]{ref}
For an event alphabet $\{a,b\}$, a <state> offering only $a$ can refuse $\{b\}$ but cannot refuse $\{a\}$. Every subset of a possible refusal is also possible. In a model without a separate successful-termination event, refusing the entire event alphabet signals <deadlock>. Refusals therefore distinguish a missing offer from an event merely not selected by the environment.
Back to article page
