// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// This module demonstrates that one has to distinguish between the surface   //
// and the depth of statements: When resuming the execution from location w   //
// under the condition that i holds, the depth, i.e., emit(o2) has to be      //
// aborted, while the surface, i.e, emit(o1) is allowed to execute due to     //
// the delayed abortion.                                                      //
// ************************************************************************** //


module RedoAbort(event ?i,!o1,!o2) {
    loop
        abort {
            emit(o1);
            w: pause;
            emit(o2);
        } when(i);
}
satisfies {
   s1 : assert o1 & !o2;
   s3 : assert A X A G o1;
   s4 : assert A X A G (o2 <-> !i);
}
drivenby {
    pause;
    emit(i);
}