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