the interface set can only occur when all component processes are able to engage in that event. For example, the process requires that and must both be able to perform event before that event can occur. So, for example, the process can engage in event and become the process while will simply deadlock. Hiding The hiding operator provides a way to abstract processes by making some events unobservable. A trivial example of hiding is which, assuming that the event doesn't appear in , simply reduces to Examples 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: A person who might choose to use a coin or card to make payments could be modelled as: 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, whereas if synchronization was only required on “coin”, we would obtain If we abstract this latter composite process by hiding the “coin” and “card” events, i.e. we get the nondeterministic process 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), nondeterminism has been introduced. Formal definition Syntax The syntax of CSP defines the “legal” ways in which processes and events may be combined. Let be an event, and be a set of events. Then the basic syntax of CSP can be defined as: Note that, in the interests of brevity, the syntax presented above omits the process, which represents divergence, as well as various operators such as alphabetized parallel, piping, and indexed choices. Formal semantics CSP has been imbued with several different formal semantics, which define the meaning of syntactically correct CSP expressions. The theory of CSP includes mutually consistent denotational semantics, algebraic semantics, and operational semantics. Denotational semantics The three major denotational models of CSP