// ************************************************************************** //
//                                                                            //
//    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 variant of Gonthier's program due to Stephen Edwards.            //
// The program shows that we need several copies of the outputs unless we     //
// abbreviate them by anonymous expressions. In the latter case, however, we  //
// need several anonymous expressions either.                                 //
// ************************************************************************** //

module Edwards(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 {
                        event a,b;
                        if(x1)
                           {if(!x2) emit(b);}
                        else emit(a);
                        case
                           ( a &  b) do emit(out_11);
                           (!a &  b) do emit(out_01);
                           ( a & !b) do emit(out_10);
                           (!a & !b) do emit(out_00);
                        default nothing;
                        p3: pause;
                     }
               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);
}