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