Editing Communicating sequential processes (section)

=== Examples ===
{{unreferenced section|date=November 2024}}
One of the archetypal CSP examples is an abstract representation of a chocolate vending machine and its interactions with a person wishing to buy some chocolate. This vending machine might be able to carry out two different events, “coin” and “choc” which represent the insertion of payment and the delivery of a chocolate respectively. A machine which demands payment (only in cash) before offering a chocolate can be written as:

<math display="block">\mathrm{VendingMachine} = \mathrm{coin} \rightarrow \mathrm{choc} \rightarrow \mathrm{STOP}</math>

A person who might choose to use a coin or card to make payments could be modelled as:

<math display="block">\mathrm{Person} = (\mathrm{coin} \rightarrow \mathrm{STOP})\; \Box\; (\mathrm{card} \rightarrow \mathrm{STOP})</math>

These two processes can be put in parallel, so that they can interact with each other. The behaviour of the composite process depends on the events that the two component processes must synchronise on. Thus,

<math display="block">\mathrm{VendingMachine} \left\vert\left[\left\{ \mathrm{coin}, \mathrm{card} \right\}\right]\right\vert \mathrm{Person} \equiv \mathrm{coin} \rightarrow \mathrm{choc} \rightarrow \mathrm{STOP}</math>

whereas if synchronization was only required on “coin”, we would obtain

<math display="block">\mathrm{VendingMachine} \left\vert\left[\left\{ \mathrm{coin} \right\}\right]\right\vert \mathrm{Person} \equiv \left (\mathrm{coin} \rightarrow \mathrm{choc} \rightarrow \mathrm{STOP}\right ) \Box \left (\mathrm{card} \rightarrow \mathrm{STOP}\right )</math>

If we abstract this latter composite process by hiding the “coin” and “card” events, i.e.

<math display="block">\left (\left (\mathrm{coin} \rightarrow \mathrm{choc} \rightarrow \mathrm{STOP}\right ) \Box \left (\mathrm{card} \rightarrow \mathrm{STOP}\right )\right ) \setminus \left\{\mathrm{coin, card}\right\}</math>

we get the nondeterministic process

<math display="block">\left (\mathrm{choc} \rightarrow \mathrm{STOP}\right ) \sqcap \mathrm{STOP}</math>

This is a process which either offers a “choc” event and then stops, or just stops. In other words, if we treat the abstraction as an external view of the system (e.g., someone who does not see the decision reached by the person), [[Nondeterministic algorithm|nondeterminism]] has been introduced.