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