// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // The following module has been discussed on SLAP04 as a program having a // // difficult schizophrenic behavior. We show its equivalence to a simplified // // version. // // ************************************************************************** // module SLAP04(event ?i,?j,?k,nat{14} !x) { weak abort loop { nat{14} a; a = 1; weak abort loop { nat{14} b; b = a+1; weak abort loop { nat{14} c; c = b+1; next(c) = (a+b)+c; w: pause; x = a; next(a) = (a+b)-c; next(b) = (a-b)+c; } when(k); } when(j); } when(i); } satisfies { observer(nat{14} a1,b1,c1,x1) { a1 = 1; b1 = 2; c1 = 3; next(c1) = 6; do { w0: pause; x1 = a1; if(!i) { if(j) { next(a1) = 1; next(b1) = 2; next(c1) = 6; } else if(k) { next(a1) = (a1+b1)-c1; next(b1) = a1+1; next(c1) = (a1+(a1+1))+(a1+2); } else { next(a1) = (a1+b1)-c1; next(b1) = (a1-b1)+c1; next(c1) = (a1+b1)+(b1+1); } } } while(!i); } equiv: assert A G (x1 == x); } drivenby drv0 { for(i=0..10) pause; }