Past exam of the computer science course of the University of Oxford / 2015 / Concurrency / 3 / c / Solution

For each node letThe required CSP alphabetized parallel composition isEach message CSP event belongs to exactly the sender's and receiver's alphabets and synchronizes those two processes. A status signal belongs only to its own node. Using the common set of all message events as an all-node synchronization alphabet would be incorrect: unrelated nodes would then have to participate in each point-to-point transfer. The initial definitions in parts (a) and (b) make every node active. Keep the message CSP events visible here; later checks can apply CSP hiding as needed.