// ************************************************************************** // // // // 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 Transfer00(int{8} a,!y) { a = 1; loop { int{16} x; x = a; next(x) = x+2; pause; y = x; next(a) = a+1; } } drivenby { // ------------------------------------------------------------------ // the behavior 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)); w00: pause; atime01 : assert((a==1) & (y==3)); w01: pause; atime02 : assert((a==2) & (y==3)); w02: pause; atime03 : assert((a==3) & (y==4)); w03: pause; atime04 : assert((a==4) & (y==5)); w04: pause; atime05 : assert((a==5) & (y==6)); w05: pause; atime06 : assert((a==6) & (y==7)); }