// ************************************************************************** // // // // 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 conditions of conditional statements // // are checked 'before' checking runtime errors in their branches. The // // program below generates the following two guarded actions: // // * 0<i&a[i+2] => error = True // // * 0<i => assert i+2<2 // // It is not trivial that the evaluation of the guard 0<i&a[i+2] does not fail// // under an environment where i==0 holds. This is only given by the fact that // // by definition of &, false&top=false holds. // // See also CondExpr1.qrz for comparison. // // ************************************************************************** // module CondStat1(nat ?i,[2]bool ?a,event !error) { if(i>0) { if(a[i+2]) emit(error); } } drivenby { nothing; }