// ************************************************************************** //
//                                                                            //
//    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 goes back to Gontier's PhD thesis. It shows that a local      //
// variable can generate arbitrarily many reincarnations if its declaration is//
// nested within loops and abortions. Gontier's original program is given also//
// in [Berr99,page 138] as program P18.                                       //
// ************************************************************************** //

module Gonthier02(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 {
                        case
                           (!x1 & !x2) do emit(out_00);
                           (!x1 &  x2) do emit(out_01);
                           ( x1 & !x2) do emit(out_10);
                           ( x1 &  x2) do emit(out_11);
                        default nothing;
                        p3: pause;
                     }
               when(x2);
            }
      when(x1);
   }
}