// ************************************************************************** //
//                                                                            //
//    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 module demonstrates the necessity to distinguish between surface and   //
// depth of a statement: While the depth of the body of the abortion statement//
// must be aborted when started in location w under condition i, its surface  //
// must still be executed, since it refers to a new incarnation of the        //
// execution.                                                                 //
// ************************************************************************** //

module RedoAbort(event i,!a,!b) {
    loop {
        abort {
            emit(a);
            w: pause;
            emit(b);
        } when(i);
    }
}