// ************************************************************************** //
//                                                                            //
//    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 Gonthier03(event !out_111,!out_110,!out_101,!out_100,
                        !out_011,!out_010,!out_001,!out_000) {
   loop {
      event x1;
      weak abort
            {
            p1: pause;
            emit(x1);
            }
         ||
            loop {
               event x2;
               weak abort
                     {
                     p2: pause;
                     emit(x2);
                     }
                  ||
                     loop {
                        event x3;
                        weak abort
                              {
                              p3: pause;
                              emit(x3);
                              }
                           ||
                              loop {
                                 case
                                    (!x1 & !x2 & !x3) do emit(out_000);
                                    (!x1 & !x2 &  x3) do emit(out_001);
                                    (!x1 &  x2 & !x3) do emit(out_010);
                                    (!x1 &  x2 &  x3) do emit(out_011);
                                    ( x1 & !x2 & !x3) do emit(out_100);
                                    ( x1 & !x2 &  x3) do emit(out_101);
                                    ( x1 &  x2 & !x3) do emit(out_110);
                                    ( x1 &  x2 &  x3) do emit(out_111);
                                 default nothing;
                                 p4: pause;
                              }
                        when(x3);
                     }
               when(x2);
            }
      when(x1);
   }
} satisfies {
   spec_out_000 : assert A G A X out_000;
   spec_out_001 : assert A G A X !out_001;
   spec_out_010 : assert A G A X !out_010;
   spec_out_011 : assert A G A X !out_011;
   spec_out_100 : assert A G A X out_100;
   spec_out_101 : assert A G A X !out_101;
   spec_out_110 : assert A G A X out_110;
   spec_out_111 : assert A G A X out_111;
}