verif/Spin/Test/eratosthenes

   1 /*
   2         The Sieve of Eratosthenes (c. 276-196 BC)
   3         Prints all prime numbers up to MAX
   4 */
   5 #define MAX     25
   6
   7 mtype = { number, eof };
   8
   9 chan root = [0] of { mtype, int };
  10
  11 proctype sieve(chan c; int prime)
  12 {       chan child = [0] of { mtype, int };
  13         bool haschild;
  14         int n;
  15
  16         printf("MSC: %d is prime\n", prime);
  17 end:    do
  18         :: c?number(n) ->
  19                 if
  20                 :: (n%prime) == 0 ->
  21                         printf("MSC: %d = %d*%d\n", n, prime, n/prime)
  22                 :: else ->
  23                         if
  24                         :: !haschild -> /* new prime */
  25                                 haschild = true;
  26                                 run sieve(child, n);
  27                         :: else ->
  28                                 child!number(n)
  29                         fi;
  30                 fi
  31         :: c?eof(0) ->
  32                 break
  33         od;
  34         if
  35         :: haschild ->
  36                 child!eof(0)
  37         :: else
  38         fi
  39 }
  40
  41 init
  42 {       int n = 2;
  43
  44         run sieve(root, n);
  45         do
  46         :: (n <  MAX) -> n++; root!number(n)
  47         :: (n >= MAX) -> root!eof(0); break
  48         od
  49 }