// ************************************************************************** //
//                                                                            //
//    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 transfered 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 Transfer01(int{8} a,!y) {
   a = 1;
   loop {
      int{8} x;
      x = a;
      next(x) = x+2;
      pause;
      y = x;
      next(a) = a+1;
   }
} satisfies {
// ------------------------------------------------------------------
// the behaviour 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);
   atime01 : assert A X ((a==1) & (y==3));
   atime02 : assert A X A X ((a==2) & (y==3));
   atime03 : assert A X A X A X ((a==3) & (y==-4));
   atime04 : assert A X A X A X A X ((a==-4) & (y==-3));
   atime05 : assert A X A X A X A X A X ((a==-3) & (y==-2));
   atime06 : assert A X A X A X A X A X A X ((a==-2) & (y==-1));
   atime07 : assert A X A X A X A X A X A X A X ((a==-1) & (y==0));
   atime08 : assert A X A X A X A X A X A X A X A X ((a==0) & (y==1));
   atime09 : assert A X A X A X A X A X A X A X A X A X ((a==1) & (y==2));
   atime10 : assert A X A X A X A X A X A X A X A X A X A X ((a==2) & (y==3));
// ------------------------------------------------------------------
   etime00 : assert (a==1) & (y==0);
   etime01 : assert E X ((a==1) & (y==3));
   etime02 : assert E X E X ((a==2) & (y==3));
   etime03 : assert E X E X E X ((a==3) & (y==-4));
   etime04 : assert E X E X E X E X ((a==-4) & (y==-3));
   etime05 : assert E X E X E X E X E X ((a==-3) & (y==-2));
   etime06 : assert E X E X E X E X E X E X ((a==-2) & (y==-1));
   etime07 : assert E X E X E X E X E X E X E X ((a==-1) & (y==0));
   etime08 : assert E X E X E X E X E X E X E X E X ((a==0) & (y==1));
   etime09 : assert E X E X E X E X E X E X E X E X E X ((a==1) & (y==2));
   etime10 : assert E X E X E X E X E X E X E X E X E X E X ((a==2) & (y==3));
// ------------------------------------------------------------------
}