// **************************************************************************
//
//    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 IncDecAdd(
    int ?x, ?y, x_sum, x1, y1
) {
    x1 = x;
    y1 = y;
    x_sum = x+y;

    while (x1>0) {
        next(x1) = x1-1;
        next(y1) = y1+1;
        ell1:pause;
    }

    while (x1<0) {
        next(x1) = x1+1;
        next(y1) = y1-1;
        ell2:pause;
    }

} satisfies {
    s1 : assert A F terminate;
    s2 : assert A G (terminate -> (y1==x_sum));
    s3 : assert A [(y1==x_sum) SW terminate];
}