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