// ************************************************************************** //
//                                                                            //
//    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 Transfer02(int a,!y) {
   a = 1;
   loop {
      int 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==5));
   atime05 : assert A X A X A X A X A X ((a==5) & (y==6));
   atime06 : assert A X A X A X A X A X A X ((a==6) & (y==7));
   atime07 : assert A X A X A X A X A X A X A X ((a==7) & (y==8));
   atime08 : assert A X A X A X A X A X A X A X A X ((a==8) & (y==9));
   atime09 : assert A X A X A X A X A X A X A X A X A X ((a==9) & (y==10));
   atime10 : assert A X A X A X A X A X A X A X A X A X A X ((a==10) & (y==11));
// ------------------------------------------------------------------
   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==5));
   etime05 : assert E X E X E X E X E X ((a==5) & (y==6));
   etime06 : assert E X E X E X E X E X E X ((a==6) & (y==7));
   etime07 : assert E X E X E X E X E X E X E X ((a==7) & (y==8));
   etime08 : assert E X E X E X E X E X E X E X E X ((a==8) & (y==9));
   etime09 : assert E X E X E X E X E X E X E X E X E X ((a==9) & (y==10));
   etime10 : assert E X E X E X E X E X E X E X E X E X E X ((a==10) & (y==11));
// ------------------------------------------------------------------
}