// ************************************************************************** // // // // 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 demonstrates that nested conditionals as shown in module // // CondStat1.qrz have a different semantics as flattened conditionals as // // shown below. The program below generates the following two guarded actions:// // * 0<i&a[i+2] => error = True // // * True => assert i+2<2 // // whereas a nested conditional as in module CondStat1.qrz generates: // // * 0<i&a[i+2] => error = True // // * 0<i => assert i+2<2 // // As in CondStat1, the evaluation of the guard 0<i&a[i+2] does not fail // // under an environment where i==0 holds, however, the assertion now fails. // // See also CondExpr2.qrz for further discussion. // // ************************************************************************** // module CondStat2(nat ?i,[2]bool ?a,event !error) { if(i>0 & a[i+2]) emit(error); } drivenby { nothing; }