| 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 |