-- Synchronous leader election protocol. -- Source: Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. -- Information and Computation 88(1), 60-87 (1990) -- The protocol models a ring of N processors with a common clock. -- The goal is to elect a leader, i.e. a uniquely designated processor, -- by sending messages around the ring. The protocol proceeds in rounds. -- During each round the processors draw a random number from the range -- {1,...,K} as an ID. If there is a unique maximal id, the processor -- with this id becomes the leader. Otherwise a new round is initiated. -- Concrete setting: N = 3, K = 2. DECL -- Disables random quantifier. define OFF = 0; -- Probability 1/K define PROB = 0.5; boole leader_found; boole leader_found_now; INIT !leader_found; DISTR R. N1 p = [ OFF -> 1, 1 -> PROB, 2 -> PROB ]: R. N2 p = [ OFF -> 1, 1 -> PROB, 2 -> PROB ]: R. N3 p = [ OFF -> 1, 1 -> PROB, 2 -> PROB ]: TRANS -- If leader found then disable random experiments -- and keep that leader found. leader_found -> (N1 = OFF and N2 = OFF and N3 = OFF); leader_found -> leader_found'; leader_found -> !leader_found_now; -- If leader was not yet found, enable all experiments. !leader_found -> (N1 != OFF and N2 != OFF and N3 != OFF); -- Check whether leader is found now. !leader_found -> ( leader_found_now <-> ( -- N1 is leader. ( (N1 > N2 and N1 > N3) -- N2 is leader. or (N2 > N1 and N2 > N3) -- N3 is leader. or (N3 > N1 and N3 > N2)) ) ); -- If election was not successful, next try. !leader_found and !leader_found_now -> !leader_found'; -- If election was successful, we found leader. !leader_found and leader_found_now -> leader_found'; TARGET leader_found;