// ************************************************************************** // // // // 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; }