// **************************************************************************
//
//    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
//
// **************************************************************************

module TerminExample04(
    int ?a, ?b, x, y
) {
    x = a;
    y = b;
    while (x>0 & y>0) {
        choose {
            next(x) = x - 1;
            next(y) = x;
        } else {
            next(x) = y - 2;
            next(y) = x + 1;
        }
        ell: pause;
    }
} satisfies {
    s1: assert A F terminate;
    s2: assert nu z. <>z;
}