// ************************************************************************** //
//                                                                            //
//    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 program shows that we can not simply stop the fixpoint computation as //
// soon as all values are known values. In the first iteration of the macro   //
// step, y will obtain the value true (due to the must-assignment), and x     //
// receives the value false due to the reaction to absence. Hence, all values //
// are known after this first iteration. However, a second iteration reveals  //
// that we also have to execute the then branch of the if-statement which     //
// results in a write conflict that changes the value of y to TOP.            //
// The program also demonstrates that we need not only the additional value   //
// BOT, but also TOP to obtain a full lattice, so that also write conflicts   //
// are properly modeled.                                                      //
// ************************************************************************** //


module top(bool ?x,!y) {
   y=true;
   if(!x) y=false;
} drivenby drv0 {
    x = false;
} drivenby drv1 {
    x = true;
}



//  ***********************************
//    macro step number 0
//  ***********************************
//    active locations: __start
//  ***********************************
//     --------------------------------
//      iteration 0 of macro step 0
//     --------------------------------
//     before executing must actions:
//         x:      BOT
//         y:      BOT
//     before reaction to absence:
//         x:      BOT
//         y:      1
//     after reaction to absence:
//         x:      0
//         y:      1
//     --------------------------------
//      iteration 1 of macro step 0
//     --------------------------------
//     before executing must actions:
//         x:      0
//         y:      1
//     before reaction to absence:
//         x:      0
//         y:      TOP
//     after reaction to absence:
//         x:      0
//         y:      TOP
//     --------------------------------
//      iteration 2 of macro step 0
//     --------------------------------
//     before executing must actions:
//         x:      0
//         y:      TOP
//     before reaction to absence:
//         x:      0
//         y:      TOP
//     after reaction to absence:
//         x:      0
//         y:      TOP
//     --------------------------------
//      -> fixpoint found (causality problem)
//      -> final environment (selected latest reincarnations)
//         x:      0
//         y:      TOP
//      -> no delayed assignments
//     --------------------------------
//  --------------------------------
//    encountered causality problem
//  --------------------------------