// ------------------------------------------------------------	//
// A simple implementation of Euclid's algorithm for computing	//
// the greatest common divisor of two given natural numbers.	//
// Note the trick to use input "a" once again in specification 	//
// "is_greatest_divisor" to implicitely quantify over all 	//
// numbers in nat[bits].					//
// ------------------------------------------------------------	//

#ifndef bits
#define bits 4
#endif

#define IsCommonDivisor(x,y,d) ((x % d)==0u) & ((y % d)==0u)

module Monitor(nat[bits] a,b,&x,&y,&g, event &ready)
implements MonitorSpec(a,x,y,g,ready) {
   x = a;
   y = b;
   Euclid(a,b,g,ready);
   next(y) = y % a;
}


spec MonitorSpec(nat[bits] a,x,y,g,event ready) {
  terminate           : A F ready;
  is_common_divisor   : A G (ready -> IsCommonDivisor(x,y,g));
  is_greatest_divisor : A G (ready & (x!=0u) & IsCommonDivisor(x,y,a) -> a<=g);
}



module Euclid(nat[bits] a,b,&x, event &ready) {
   nat[bits] y;
   x = a;
   y = b;
   do {
      if(x>=y)
         next(x) = x-y;
      else
         next(y) = y-x;
      pause;
   } while(x!=0u & y!=0u);
   if(x==0u) next(x) = y;
   pause;
   emit ready;
}