// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// Compute the integer square root. The idea behind the algorithm given below //
// is as follows: it can be easily proved that n^2 = sum(i=1..root(n)} 2i+1   //
// holds, i.e., that the square numbers are the sums of the first odd numbers //
// where root(n) summands have to be added. Hence, we simply compute the sum  //
// of the first odd numbers and stop as soon as this sum becomes larger than  //
// the given number. The computation time is therefore O(root(a)).            //
// In contrast to SquareRoot1, we introduce a further local variable n that is//
// invariantly n=2*r+1, so that we avoid the multiplication operation with r. //
// This way, we only need additions to compute the square root.               //
// ************************************************************************** //

macro N = 1000000;

module SquareRoot2(nat{N} ?a,r,event !rdy) {
    nat{N*2} s;
    nat{N} n;
    r = 0;  // preliminary root
    n = 1;  // invariant: n = 2*r+1
    s = 1;  // invariant: s = sum(int i=1..r+1} 2i+1
    while(s <= a) {
        next(r) = r + 1;
        next(n) = n + 2;
        next(s) = s + n + 2;
        pause;
    }
    emit(rdy);
    assert(r*r <= a & a < (r+1)*(r+1));
}
drivenby {
    a = 900;
    await(rdy);
}
drivenby {
    a = 4568;
    await(rdy);
}