// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// First, 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.                                                 //
// In addition to Schizo00, an immediate assignment that is executed in the   //
// surface of a local declaration and that overlaps with the assignment       //
// next(x) := 3 at termination time, does NOT yield a write conflict.         //
// ************************************************************************** //

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