= CSP failures semantics
{c}
<CSP failures semantics> augments visible traces with <CSP refusal set>[refusal information]. In the stable failures model, a pair $(s,X)$ means that after visible trace $s$, the process can reach a stable <state> with no internal transition and no offered event in $X$. It records a possible refusal, not a requirement that every <state> reached after $s$ refuse $X$.<The CSP View of the World in the FDR2 User Manual>[§1.2, stable failures model]{ref}
<CSP choice>[External choice] between offering $a$ and offering $b$ cannot initially refuse either offered event. <CSP choice>[Internal choice] between the same branches may select the $b$ branch and refuse $a$. Their visible trace sets can agree even though these refusals differ. Failures-divergences semantics additionally records possible infinite internal activity; it is a distinct model.
Back to article page
