verif/Spin/Test/sort

   1 /*
   2  * A program to sort concurrently N "random" numbers
   3  * The reduced space and time should be linear in the
   4  * number of processes, and can be reduced when the length of
   5  * the buffer queues is increased.
   6  * In full search it should be exponential.
   7  */
   8
   9 #define N       7                       /* Number of Proc */
  10 #define L       10                      /* Size of buffer queues */
  11 #define RANDOM  (seed * 3 + 14) % 100   /* Calculate "random" number */
  12
  13 chan q[N] = [L] of {byte};
  14
  15 proctype left(chan out)                 /* leftmost process, generates random numbers */
  16 {       byte counter, seed;
  17
  18         xs out;
  19
  20         counter = 0; seed = 15;
  21         do
  22         :: out!seed ->                  /* output value to the right */
  23                 counter = counter + 1;
  24                 if
  25                 :: counter == N -> break
  26                 :: counter != N -> skip
  27                 fi;
  28                 seed = RANDOM           /* next "random" number */
  29         od
  30 }
  31
  32 proctype middle(chan in, out; byte procnum)
  33 {       byte counter, myval, nextval;
  34
  35         xs out;
  36         xr in;
  37
  38         counter = N - procnum;
  39         in?myval;                               /* get first value from the left */
  40         do
  41         :: counter > 0 ->
  42                 in?nextval;                     /* upon receipt of a new value */
  43                 if
  44                 :: nextval >= myval -> out!nextval
  45                 :: nextval <  myval ->
  46                         out!myval;
  47                         myval=nextval           /* send bigger, hold smaller */
  48                 fi;
  49                 counter = counter - 1
  50         :: counter == 0 -> break
  51         od
  52 }
  53
  54 proctype right(chan in) /* rightmost channel */
  55 {       byte biggest;
  56
  57         xr in;
  58
  59         in?biggest              /* accepts only one value, which is the biggest */
  60 }
  61
  62 init {
  63         byte proc=1;
  64
  65         atomic {
  66                 run left ( q[0] );
  67                 do
  68                 :: proc < N ->
  69                         run middle ( q[proc-1] , q[proc], proc );
  70                         proc = proc+1
  71                 :: proc == N -> break
  72                 od;
  73                 run right ( q[N-1] )
  74         }
  75 }