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