// ************************************************************************** //
//                                                                            //
//    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 module shows that the correct surface value has to be selected when a //
// local declaration proceeds to the depth of its body. Note that when the    //
// program is at location w, the assignment to y1 assigns the value of the    //
// surface that has been computed right before and NOT the value that will be //
// assigned to c when re-entering the loop, although this assignment happens  //
// at the same point of time.                                                 //
// ************************************************************************** //


module Schizo02(bool ?a,?b,event nat{4} !y0,!y1) {
  y1 = 1;
  weak abort
    loop
      weak abort
        loop {
           nat{4} c;
           case
              (a) do c = 1;
                  (b) do c = 2;
               default   c = 3;
           y0 = c;
           w: pause;
           y1 = c;
        }
      when(b);
  when(a);
} satisfies {
  y0_vals: assert A G((y0==1) | (y0==2) | (y0==3));
  y1_vals: assert A G((y1==1) | (y1==2) | (y1==3));
  init   : assert (y1==1) & (a?(y0==1):(b?(y0==2):(y0==3)));
  invar_y0: assert A[(a?(y0==1):(b?(y0==2):(y0==3))) WU terminate];
  term_a : assert A[( a    -> X (y1==1)) WU terminate];
  term_b : assert A[(!a& b -> X (y1==2)) WU terminate];
  invar  : assert A[(!a&!b -> X (y1==3)) WU terminate];
}