// ************************************************************************** //
//                                                                            //
//    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 checks that the correct values are transferred from a         //
// reincarnation to the depth. Note that when the assignment to y is done,    //
// there will also be done the assignment x := a in the surface of the new    //
// scope of x. That must not be seen in y!                                    //
// ************************************************************************** //

module Transfer00(int{8} a,!y) {
   a = 1;
   loop {
      int{16} x;
      x = a;
      next(x) = x+2;
      pause;
      y = x;
      next(a) = a+1;
   }
}
drivenby {
// ------------------------------------------------------------------
// the behavior is a simple single computation that is as follows:
// note that time10 and time02 refer to the same state!
// ------------------------------------------------------------------
   atime00 : assert((a==1) & (y==0));
   w00: pause;
   atime01 : assert((a==1) & (y==3));
   w01: pause;
   atime02 : assert((a==2) & (y==3));
   w02: pause;
   atime03 : assert((a==3) & (y==4));
   w03: pause;
   atime04 : assert((a==4) & (y==5));
   w04: pause;
   atime05 : assert((a==5) & (y==6));
   w05: pause;
   atime06 : assert((a==6) & (y==7));
}