// ************************************************************************** //
//                                                                            //
//    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 program below suffers from the following causality problem:            //
// The assignment "y = 0" depends on the termination of the inner loop, which //
// in turn depends on the value of y. So, reaching location p2 brings the     //
// simulator to a situation that cannot be resolved.                          //
// ************************************************************************** //


module Z02(nat{8} y) {
    loop {
        y = 0;
        while(y < 7) {
            next(y) = y + 1;
            p1: pause;
            p2: pause;  // if this is removed, a write conflict occurs in step 7
        }
    }
}
drivenby {
    for(i=1..10)
        pause;
}