verif/Spin/Test/leader_trace

   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 notrace {
  16         do
  17         :: q[0]?one,_
  18         :: q[0]?two,_ -> break
  19         od;
  20         do
  21         :: q[0]?two,_
  22         :: q[0]?winner,_ -> break
  23         od
  24 }
  25
  26 proctype node (chan in, out; byte mynumber)
  27 {       bit Active = 1, know_winner = 0;
  28         byte nr, maximum = mynumber, neighbourR;
  29
  30         xr in;
  31         xs out;
  32
  33         printf("MSC: %d\n", mynumber);
  34         out!one(mynumber);
  35 end:    do
  36         :: in?one(nr) ->
  37                 if
  38                 :: Active ->
  39                         if
  40                         :: nr != maximum ->
  41                                 out!two(nr);
  42                                 neighbourR = nr
  43                         :: else ->
  44                                 /* Raynal p.39:  max is greatest number */
  45                                 assert(nr == N);
  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         atomic {
  86                 proc = 1;
  87                 do
  88                 :: proc <= N ->
  89                         run node (q[proc-1], q[proc%N], (N+I-proc)%N+1);
  90                         proc++
  91                 :: proc > N ->
  92                         break
  93                 od
  94         }
  95 }
  96