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