// ************************************************************************** //
//                                                                            //
//    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 is similar to SurfaceSelection1.qrz. The difference is that   //
// the assignments to the local variable x are delayed. Again, the problem is //
// that several surfaces of the local declaration of x overlap, and each of   //
// them makes an assignment to next(x).                                       //
// Note that this is no write conflict, since we have different scopes. The   //
// problem is thereby that the output variable y will obtain the correct value//
// at the next point of time. The correct value has to be stored in x so that //
// y can take it after entering the local declaration.                        //
// ************************************************************************** //

module SurfaceSelection2(event in1,in2,in3, bv{2} !y) {
  do {
     event x0;
        {
        pause;
        emit(x0);
        }
     ||
        do {
           event x1;
              {
              pause;
              emit(x1);
              }
           ||
              do {
                 bv{2} x;
                 case
                    (!x1 & !x0) do x=0b00;
                    (!x1 &  x0) do x=0b01;
                    ( x1 & !x0) do x=0b10;
                    ( x1 &  x0) do x=0b11;
                 default nothing;
                 pause;
                 y = x;
              } while(in3);
        } while(in2);
  } while(in1);
} satisfies {
   time00 : assert (y == 0b00);
   time01 : assert A X (y == 0b00);
   time02 : assert A X (
                 ( in3               -> A X (y == 0b11)) &
                 (!in3 &  in2        -> A X (y == 0b01)) &
                 (!in3 & !in2 &  in1 -> A X (y == 0b00)) &
                 (!in3 & !in2 & !in1 -> A X (y == 0b00))
                );
}