// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// This module implements a naive primality test that checks divisibility with//
// all possible divisors. It is first tested whether the given input number p //
// is divisible by 2 and 3. If so, it is clearly not a prime number.          //
// Otherwise, note that every prime number d other than 2 and 3 can be written//
// as d=6*x+r where x and r are the quotient and remainder of the division of //
// d by 6. This holds since the cases r=0,2,4 lead to an even number d, and   //
// the case r=3 leads to 6*x+3=3(2*x+1) which is divisible by 3. So, after    //
// testing divisibility by 2 and 3, it is sufficient to test divisibility by  //
// the numbers pm1=6*x+1 and pm5=6*x+5. If the module terminates with noprime //
// then either 2,3,pm1 or pm5 is a divisor.                                   //
// ************************************************************************** //

macro N = 1000000;

module Primality(nat{N} ?p,event prime,noprime) {
    nat{N} pm1,pm5,root,new_root;
    case
        (p==0)   do emit(noprime);
        (p==1)   do emit(noprime);
        (p%2==0) do emit(noprime);
        (p%3==0) do emit(noprime);
        default {
            // compute the square root of p
            new_root = p-2;
            do {
                next(new_root) = (new_root + (p / new_root)) / 2;
                next(root) = new_root;
                pause;
            } while(new_root < root);
            // test whether pm1=6x+1 or pm5=6x+5 divides p 
            pm1 = 1;
            pm5 = 5;
            do {
                next(pm1) = pm1 + 6;
                next(pm5) = pm5 + 6;
                pause;
                noprime = (p%pm1==0 | p%pm5==0);
            } while(!noprime & pm5<root);
            if(!noprime)
                emit(prime);
        }
}
drivenby {
    p=999983;
    immediate await(prime | noprime);
}
drivenby {
    p=999997;
    immediate await(prime | noprime);
}