trunk/verif/Spin/Test/leader

   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
   6 #define N       5       /* nr of processes (use 5 for demos) */
   7 #define I       3       /* node given the smallest number    */
   8 #define L       10      /* size of buffer  (>= 2*N) */
   9
  10 mtype = { one, two, winner };
  11 chan q[N] = [L] of { mtype, byte};
  12
  13 byte nr_leaders = 0;
  14
  15 proctype node (chan in, out; byte mynumber)
  16 {       bit Active = 1, know_winner = 0;
  17         byte nr, maximum = mynumber, neighbourR;
  18
  19         xr in;
  20         xs out;
  21
  22         printf("MSC: %d\n", mynumber);
  23         out!one(mynumber);
  24 end:    do
  25         :: in?one(nr) ->
  26                 if
  27                 :: Active ->
  28                         if
  29                         :: nr != maximum ->
  30                                 out!two(nr);
  31                                 neighbourR = nr
  32                         :: else ->
  33                                 /* Raynal p.39:  max is greatest number */
  34                                 assert(nr == N);
  35                                 know_winner = 1;
  36                                 out!winner,nr;
  37                         fi
  38                 :: else ->
  39                         out!one(nr)
  40                 fi
  41
  42         :: in?two(nr) ->
  43                 if
  44                 :: Active ->
  45                         if
  46                         :: neighbourR > nr && neighbourR > maximum ->
  47                                 maximum = neighbourR;
  48                                 out!one(neighbourR)
  49                         :: else ->
  50                                 Active = 0
  51                         fi
  52                 :: else ->
  53                         out!two(nr)
  54                 fi
  55         :: in?winner,nr ->
  56                 if
  57                 :: nr != mynumber ->
  58                         printf("MSC: LOST\n");
  59                 :: else ->
  60                         printf("MSC: LEADER\n");
  61                         nr_leaders++;
  62                         assert(nr_leaders == 1)
  63                 fi;
  64                 if
  65                 :: know_winner
  66                 :: else -> out!winner,nr
  67                 fi;
  68                 break
  69         od
  70 }
  71
  72 init {
  73         byte proc;
  74         atomic {
  75                 proc = 1;
  76                 do
  77                 :: proc <= N ->
  78                         run node (q[proc-1], q[proc%N], (N+I-proc)%N+1);
  79                         proc++
  80                 :: proc > N ->
  81                         break
  82                 od
  83         }
  84 }
  85