```// ************************************************************************** //
//                                                                            //
//    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));
// ------------------------------------------------------------------
}
```