1 /* Dolev, Klawe & Rodeh for leader election in unidirectional ring
2 * `An O(n log n) unidirectional distributed algorithm for extrema
3 * finding in a circle,' J. of Algs, Vol 3. (1982), pp. 245-260
5 * Randomized initialization added -- Feb 17, 1997
8 #define elected (nr_leaders > 0)
9 #define noLeader (nr_leaders == 0)
10 #define oneLeader (nr_leaders == 1)
16 * [] (noLeader U oneLeader)
21 #define N 5 /* number of processes in the ring */
22 #define L 10 /* 2xN */
25 mtype = { one, two, winner };
26 chan q[N] = [L] of { mtype, byte};
28 proctype node (chan in, out; byte mynumber)
29 { bit Active = 1, know_winner = 0;
30 byte nr, maximum = mynumber, neighbourR;
35 printf("MSC: %d\n", mynumber);
57 :: neighbourR > nr && neighbourR > maximum ->
69 printf("MSC: LOST\n");
71 printf("MSC: LEADER\n");
73 assert(nr_leaders == 1)
77 :: else -> out!winner,nr
85 byte Ini[6]; /* N<=6 randomize the process numbers */
88 I = 1; /* pick a number to be assigned 1..N */
91 if /* non-deterministic choice */
92 :: Ini[0] == 0 && N >= 1 -> Ini[0] = I
93 :: Ini[1] == 0 && N >= 2 -> Ini[1] = I
94 :: Ini[2] == 0 && N >= 3 -> Ini[2] = I
95 :: Ini[3] == 0 && N >= 4 -> Ini[3] = I
96 :: Ini[4] == 0 && N >= 5 -> Ini[4] = I
97 :: Ini[5] == 0 && N >= 6 -> Ini[5] = I /* works for up to N=6 */
100 :: I > N -> /* assigned all numbers 1..N */
107 run node (q[proc-1], q[proc%N], Ini[proc-1]);
117 /* !(<>[]oneLeader) -- a sample LTL property */
123 :: !oneLeader -> goto accept