// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// Yet another variant of Gonthier's program with delayed emissions.          //
// ************************************************************************** //

module Schizo08(event !out_11,!out_10,!out_01,!out_00) {
   loop {
      event x1;
      weak abort
            {
            pause;
            emit(x1);
            }
         ||
            loop {
               event x2;
               weak abort
                     {
                     pause;
                     emit(x2);
                     }
                  ||
                     loop {
                        event a,b;
                        if(x1) emit next(a);
                        if(x2) emit next(b);
                        pause;
                        case
                           ( a &  b) do emit(out_11);
                           ( a & !b) do emit(out_10);
                           (!a &  b) do emit(out_01);
                           (!a & !b) do emit(out_00);
                        default nothing;
                     }
               when(x2);
            }
      when(x1);
   }
} satisfies {
   initial : assert !out_11 & !out_10 & !out_01 & !out_00;
   after : assert A G A X (!out_11 & !out_10 & !out_01 & out_00);
}