// ************************************************************************** // // // // 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&0<i-1 => error = True // // * 0<i => assert 1<=i // // It is not trivial that the evaluation of the guard 0<i&0<i-1 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. The assertion is not evaluated // // since its guard is false. // // See also CondExpr0.qrz for comparison. // // ************************************************************************** // module CondStat0(nat ?i,event !error) { if(i>0) { if(i-1>0) emit(error); } } drivenby { nothing; }