// ************************************************************************** // // // // 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 module below extends the discussion of the semantics of conditional // // statements and expressions. It shows the behavior of conditionals whose // // conditions evaluate to TOP. The module has semantic problems, which is // // seen by its generated guarded actions: // // True => b = 1 // // True => c = 1 // // True => d = 1==5/a?b:c // // True => assert !(a==0) // // Indeed, the fixpoint iteration yields an environment with a==0, since // // the reaction to absence assigns this value to a. Thus, the assertion fails.// // ************************************************************************** // module CondExpr5(nat b,c,d) { nat a; b = 1; c = 1; d = (5/a==1?b:c); } drivenby { nothing; }