// =======================================================
// Compute the integer square root. The idea behind the
// algorithm given below is as follows: it can be easily
// proved that n^2 = sum(int i=1..r} 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.
// =======================================================

#ifndef bits
#define bits 4
#endif


module Monitor(nat[bits] a,&b,&r, event &correct)
implements MonitorSpec(correct)
{
   b = a;
   SquareRoot(a,r);
   if(r*r<=b & b<(r+1u)*(r+1u))
      emit correct;
}

spec MonitorSpec(event correct) {
   IsCorrect  : A F correct;
}


module SquareRoot(nat[bits] a,&r) {
   nat[bits] sq;
   nat[bits+bits] sum_2rplus1;
   sq = a;
   r = 0u;
   sum_2rplus1 = 0u;
   while(sum_2rplus1 < sq) {
      next(r) = r+1u;
      next(sum_2rplus1) = sum_2rplus1+r+r+1u;
      pause;
   }
   if(sq < sum_2rplus1) {
      next(r) = r-1u;
      pause;
   }
}