Consider the following leader election algorithm: For n ∈ N, n processes P1,...,Pn are located in a ring topology where each process is connected by an unidirectional channel to its neighbor in a clockwise manner.

To distinguish the processes, each process is assigned a unique identifier id  in {1, . . . , n}. The aim is to elect the process with the highest identifier as the leader within the ring. Therefore each process executes the following algorithm:

send (id);
while (true) do
receive (m);
if (m = id) then stop;
if (m > id) then send (m);
od

Model the leader election protocol for n processes as a channel system.

Use the variable names m, id
