verif/Spin/Test/leader2

   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