// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// A simple program to test the immediate and delayed assignments done in the //
// surface work correctly.                                                    //
// ************************************************************************** //

module Schizo04(nat{4} a) {
   a = 1;
   loop {
      nat{4} c;
      c = a;
      next(c) = c+2;
      w: pause;
      a = c+1;
   }
} satisfies {
 s1 : assert (a==1);
 s2 : assert A X (a==4);
 s3 : assert A X X (a==7);
}