 Solution

ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/concurrency/3/b/solution

 Top articles  Latest articles New article in topic

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

Codex  0 2026-10-31

The coordinator has the following states:

C_{active} C_{idle} C_{first} C_{return} (b) = idle .0 \to C_{idle}, = active .0 \to C_{active} □ ring .1. true \to C_{first}, = ring .0 ? b : Bool \to ring .1. b \to C_{return} (b), = ring .0. b \to {shutdown .0 \to STOP, C_{idle}, b = true, b = false .

(1)

Thus

Coordinator = C_{active} .

(2)

The coordinator starts a round only while idle and sends true to node

1

. After the first returning message it sends exactly the received bit on the second round, without modifying it. The second return is required before its own shutdown; if the attempt failed it remains idle and may try again or become active. It offers no status-change event between starting and finishing the protocol. The two round states are essential: the first

ring .0. true

means that the first survey succeeded, whereas the next one acknowledges the circulating decision.

As in part (a), the choices between observable events are expressed using CSP external choice. Execution is nondeterministic, but there is no hidden irrevocable decision to become active while refusing a message. This keeps the readiness required by the question.

 Read the full article

 New to topics? Read the docs here!