trunk/verif/Spin/Test/petersonN

   1 /* Peterson's algorithm for N processes - see Lynch's book, p. 284 */
   2
   3 #ifndef N
   4         #define N       3       /* nr of processes */
   5 #endif
   6
   7 byte turn[N], flag[N];
   8
   9 byte ncrit;     /* auxiliary var to check mutual exclusion */
  10
  11 active [N] proctype user()
  12 {       byte j, k;
  13         /* without never claims, _pid's are: 0 .. N-1 */
  14 again:
  15         k = 0;  /* count max N-1 rounds of competition */
  16         do
  17         :: k < N-1 ->
  18                 flag[_pid] = k;
  19                 turn[k] = _pid;
  20
  21                 j = 0;          /* for all j != _pid */
  22                 do
  23                 :: j == _pid ->
  24                         j++
  25                 :: j != _pid ->
  26                         if
  27                         :: j < N ->
  28                                 (flag[j] < k || turn[k] != _pid);
  29                                 j++
  30                         :: j >= N  ->
  31                                 break
  32                         fi
  33                 od;
  34                 k++
  35         :: else ->      /* survived all N-1 rounds */
  36                 break
  37         od;
  38
  39         ncrit++;
  40         assert(ncrit == 1);     /* critical section */
  41         ncrit--;
  42
  43         flag[_pid] = 0;
  44         goto again
  45 }