```// ************************************************************************** //
//                                                                            //
//    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);
}
```