// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// The following module implements the extended Euclidean algorithm: Given two//
// integers a and b, the algorithm computes a triple (u,v,g) such that        //
// u*a + v*b = gcd(a,b). The computation is based on the constructive proof   //
// of the Lemma of Bézout. The core of the algorithm is however Euclid's      //
// algorithm which in turn is based on the fact that the common divisors of a //
// and b are the common divisors of b and (a%b):                              //
//  * Divisors(a,b) <= Divisors(b,a%b) holds, since x*t=a, y*t=b, and a=q*b+r //
//    imply x*t = q*y*t+r, i.e., r = (x-q*y) * t so that each common divisor t//
//    of a and b also divides r = a%b.                                        //
//  * Divisors(b,a%b) <= Divisors(a,b) holds, since x*t=b, y*t=r, and a=q*b+r //
//    imply a = q*x*t+y*t = (q*x+y)*t, so that each common divisor t          //
//    of b and r=a%b also divides a.                                          //
// Thus, gcd(a,b) = gcd(b,a%b) which is the recursive step of the Euclidean   //
// algorithm. The invariants maintained in the algorithm shown below are due  //
// to Bézout's Lemma and moreover compute the numbers u and v.                //
// ************************************************************************** //

module ExtEuclid(int ?a,?b,u,v,g,event !rdy) {
    int m,n,q,s,t;

    m = a;
    n = b;
    u = 1;
    v = 0;
    s = 0;
    t = 1;
    assert(m == u*a + v*b);
    assert(n == s*a + t*b);

    // The loop maintains the following invariants:
    //    (1) m == u*a + v*b
    //    (2) n == s*a + t*b
    //    (3) gcd(m,n) = gcd(a,b)
    // Note that (3) is invariant since gcd(m,n) = gcd(n,m%n), and the other
    // invariants are immediately seen by expanding the assignments.
    
    while(n!=0) {
        q = m / n;
        next(m) = n;
        next(n) = m - q * n;
        next(u) = s;
        next(v) = t;
        next(s) = u - q * s;
        next(t) = v - q * t;
        pause;
        assert(m == u*a + v*b);
        assert(n == s*a + t*b);
    }
    // since n=0 holds, we conclude the following from the invariants
    //    (1) m == u*a + v*b
    //    (2) 0 == s*a + t*b
    //    (3) gcd(m,0) = m = gcd(a,b)
    g = m;
    emit(rdy);
}
drivenby {
    a = 99;
    b = 78;
    immediate await(rdy);
    assert(u*a+v*b==g);
    assert(a%g==0 & b%g==0);
}
drivenby {
    a = 683;
    b = 147;
    immediate await(rdy);
    assert(u*a+v*b==g);
    assert(a%g==0 & b%g==0);
}