0b55f123 |
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 |
4 | |
5 | * Randomized initialization added -- Feb 17, 1997 |
6 | */ |
7 | |
8 | #define elected (nr_leaders > 0) |
9 | #define noLeader (nr_leaders == 0) |
10 | #define oneLeader (nr_leaders == 1) |
11 | |
12 | /* sample properties: |
13 | * ![] noLeader |
14 | * <> elected |
15 | * <>[]oneLeader |
16 | * [] (noLeader U oneLeader) |
17 | */ |
18 | |
19 | byte nr_leaders = 0; |
20 | |
21 | #define N 5 /* number of processes in the ring */ |
22 | #define L 10 /* 2xN */ |
23 | byte I; |
24 | |
25 | mtype = { one, two, winner }; |
26 | chan q[N] = [L] of { mtype, byte}; |
27 | |
28 | proctype node (chan in, out; byte mynumber) |
29 | { bit Active = 1, know_winner = 0; |
30 | byte nr, maximum = mynumber, neighbourR; |
31 | |
32 | xr in; |
33 | xs out; |
34 | |
35 | printf("MSC: %d\n", mynumber); |
36 | out!one(mynumber); |
37 | end: do |
38 | :: in?one(nr) -> |
39 | if |
40 | :: Active -> |
41 | if |
42 | :: nr != maximum -> |
43 | out!two(nr); |
44 | neighbourR = nr |
45 | :: else -> |
46 | know_winner = 1; |
47 | out!winner,nr; |
48 | fi |
49 | :: else -> |
50 | out!one(nr) |
51 | fi |
52 | |
53 | :: in?two(nr) -> |
54 | if |
55 | :: Active -> |
56 | if |
57 | :: neighbourR > nr && neighbourR > maximum -> |
58 | maximum = neighbourR; |
59 | out!one(neighbourR) |
60 | :: else -> |
61 | Active = 0 |
62 | fi |
63 | :: else -> |
64 | out!two(nr) |
65 | fi |
66 | :: in?winner,nr -> |
67 | if |
68 | :: nr != mynumber -> |
69 | printf("MSC: LOST\n"); |
70 | :: else -> |
71 | printf("MSC: LEADER\n"); |
72 | nr_leaders++; |
73 | assert(nr_leaders == 1) |
74 | fi; |
75 | if |
76 | :: know_winner |
77 | :: else -> out!winner,nr |
78 | fi; |
79 | break |
80 | od |
81 | } |
82 | |
83 | init { |
84 | byte proc; |
85 | byte Ini[6]; /* N<=6 randomize the process numbers */ |
86 | atomic { |
87 | |
88 | I = 1; /* pick a number to be assigned 1..N */ |
89 | do |
90 | :: I <= 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 */ |
98 | fi; |
99 | I++ |
100 | :: I > N -> /* assigned all numbers 1..N */ |
101 | break |
102 | od; |
103 | |
104 | proc = 1; |
105 | do |
106 | :: proc <= N -> |
107 | run node (q[proc-1], q[proc%N], Ini[proc-1]); |
108 | proc++ |
109 | :: proc > N -> |
110 | break |
111 | od |
112 | } |
113 | } |
114 | |
115 | #if 0 |
116 | |
117 | /* !(<>[]oneLeader) -- a sample LTL property */ |
118 | |
119 | never { |
120 | T0: |
121 | if |
122 | :: skip -> goto T0 |
123 | :: !oneLeader -> goto accept |
124 | fi; |
125 | accept: |
126 | if |
127 | :: skip -> goto T0 |
128 | fi |
129 | } |
130 | #endif |