// **************************************************************************
//
//    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 SEFM_ExampleC2(
    int ?x, y, event !go
) {
    ell0: await (x>=1);
    y = x;
    emit (go);
    always
        next(y) = y+1;
} satisfies {
    s1 : assert A G (go -> A G !(y==0));
}