Editing Communicating sequential processes (section)

==== Stable failures model ====

The ''stable failures model'' extends the traces model with refusal sets, which are sets of events <math>X \subseteq \Sigma</math> that a process can refuse to perform. A ''failure'' is a pair <math>\left(s,X\right)</math>, consisting of a trace {{mvar|s}}, and a refusal set {{mvar|X}} which identifies the events that a process may refuse once it has executed the trace {{mvar|s}}. The observed behavior of a process in the stable failures model is described by the pair <math>\left(\mathrm{traces}\left(P\right), \mathrm{failures}\left(P\right)\right)</math>. For example,

<math display="block">\mathrm{failures}\left(\left(a \rightarrow \mathrm{STOP}\right) \Box \left(b \rightarrow \mathrm{STOP}\right)\right) = \left\{\left(\langle\rangle,\emptyset\right), \left(\langle a \rangle, \left\{a,b\right\}\right), \left(\langle b \rangle,\left\{a,b\right\}\right) \right\}</math>
<math display="block">\mathrm{failures}\left(\left(a \rightarrow \mathrm{STOP}\right) \sqcap \left(b \rightarrow \mathrm{STOP}\right)\right) = \left\{ \left(\langle\rangle,\left\{a\right\}\right), \left(\langle\rangle,\left\{b\right\}\right), \left(\langle a \rangle, \left\{a,b\right\}\right), \left(\langle b \rangle,\left\{a,b\right\}\right) \right\}</math>