// ************************************************************************** //
//                                                                            //
//    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 program is due to Gerard Berry. The "emit o1" statement is executed   //
// twice at the second point of time, where the threads are resumed from      //
// locations loc1 and loc3, respectively. It may become a problem when        //
// "emit o1" is replaced with another instantaneous statement.                //
// ************************************************************************** //

module Schizo05(event !o1,!o2) {
    event x;
    loop {
        event t;
        weak immediate abort {
            event s;
                {
                if(x) emit(s);
                else pause;
                if(s) pause; || emit(o1);
                emit(o2);
                }
             ||
                {
                pause;
                emit(x);
                emit(t);
                }
        } when(t);
    }
} satisfies {
  s0 : assert !o1 & !o2;
  s1 : assert A X A G (o1 & o2);
}