verif/Spin/Test/erathostenes

   1 /*
   2         The Sieve of Erathostenes
   3         Prints all prime numbers up to PRIME_MAX
   4 */
   5 #define PRIME_MAX       100
   6
   7 chan count = [0] of { int };
   8 byte tries = 2;
   9
  10 proctype sieve(chan c; int prime)
  11 {       int i, haschild;
  12
  13 end:    do
  14         :: c?i ->
  15                 if
  16                 :: (i%prime) ->
  17                         if
  18                         :: !haschild ->
  19                                 /* found a new prime */
  20                                 printf("MSC: %d\n", i);
  21                                 haschild++;
  22                                 chan child = [0] of { int };
  23                                 run sieve(child, i);
  24                         :: else ->
  25                                 child!i
  26                         fi;
  27                 :: else
  28                         /* i is divisible by prime */
  29                 fi
  30         od
  31 }
  32
  33 init
  34 {
  35         run sieve(count, 2);
  36         do
  37         :: (tries <  PRIME_MAX) -> count!tries; tries++
  38         :: (tries >= PRIME_MAX) -> break
  39         od
  40 }