// ************************************************************************** //
//                                                                            //
//    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 is a variation of Edward's variation of Gonthier's program.           //
// In contrast to Edward's program, we use state variables below.             //
// ************************************************************************** //

module Schizo07(event !out_11,!out_10,!out_01,!out_00) {
   loop {
      event x1;
      weak abort
            {
            p1: pause;
            emit(x1);
            }
         ||
            loop {
               event x2;
               weak abort
                     {
                     p2: pause;
                     emit(x2);
                     }
                  ||
                     loop {
                        bool a,b;
                        a = x1;
                        b = x2;
                        p3: 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);
}