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