// ************************************************************************** //
//                                                                            //
//    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 program may cause problems in code generators in that they   //
// believe that there is a cyclic dependency between v and y. However, the    //
// scope of v breaks this dependency, which requires to rename also the first //
// surface that is executed initially.                                        //
// The program generates the following guarded actions:                       //
//    init:   True => next(w) = True                                          //
//            True => y = x                                                   //
//            True => v = y                                                   //
//    main:   w => next(w) = True                                             //
//            w => y = v                                                      //
//            w => v@0 = y                                                    //
// Thus, in the initial step, there is a dependency from x --> y, while in the//
// later steps there are dependencies v --> y and y --> v@0, i.e., to the     //
// reincarnation of v. The distinction of v and v@0 makes the main steps      //
// acyclic, and also if an equation system is generated, it will only have a  //
// pseudo-cycle:                                                              //
//	 v@0 := if w then y else false                                            //
//	 v   := if start then y else v'                                           //
//	 y   := if start then x else (if w then v else y')                        //
//	 next(v') := if w then v@0 else v                                         //
//	 next(y') := y                                                            //
// ************************************************************************** //


module PseudoCycle(bool ?x, y) {
    y = x;
    loop {
        bool v;
        v = y;
        w: pause;
        y = v;
    }
}
drivenby drv0 {
    x = false;
    for(i=0..5)
        pause;
}
drivenby drv1 {
    x = true;
    for(i=0..5)
        pause;
}