// ************************************************************************** //
//                                                                            //
//    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 shows that values of local variables that are assigned in the //
// surface of the local declaration have to be carefully distinguished. The   //
// local variable x can several reincarnations that receive different values  //
// according to the current incarnations of the local events x0 and x1.       //
// 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 SurfaceSelection1(event ?in1,?in2,?in3, bv{2} y) {
  do {
     event x0;
        {
        w0: pause;
        emit(x0);
        }
     ||
        do {
           event x1;
              {
              w1: 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;
                     w: pause;
                 y = x;
              } while(in3);
        } while(in2);
  } while(in1);
} drivenby drv0 {
    pause;
    in1 = false;
    in2 = false;
    in3 = false;
    pause;
} drivenby drv1 {
    pause;
    in1 = false;
    in2 = false;
    in3 = true;
    pause;
} drivenby drv2 {
    pause;
    in1 = false;
    in2 = true;
    in3 = false;
    pause;
} drivenby drv3 {
    in1 = false;
    in2 = false;
    in3 = false;
    pause;
} drivenby drv4 {
    in1 = false;
    in2 = false;
    in3 = false;
    pause;
}