// ************************************************************************** //
//                                                                            //
//    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 module shows that delayed assignments on local variables that are     //
// executed at termination time of the local declaration have no effect,      //
// hence, they are dead code.                                                 //
// ************************************************************************** //

module Schizo00(nat{4} !y) {
   loop {
      nat{4} x;
      y = x;            // y receives the default value of x
      next(x) = 2;
      w1: pause;
      y = x;            // y will be 2
      w2: pause;
      next(x) = 3;      // this is dead code!
   }
}
satisfies {
  step0: assert (y==0);
  step1: assert A G((y==0) -> X(y==2));
  step2: assert A G((y==2) -> X(y==0));
}