// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// This extends the discussion on modules CondStat1.qrz and CondStat2.qrz.    //
// Here, it is checked that the immediate effect of assignments takes place,  //
// which is given in that array access remains unknown until the index        //
// expression becomes known. The program generates the following guarded      //
// actions:                                                                   //
//        True   => i = 1                                                     //
//        a[i-1] => error = True                                              //
//        True   => assert i-1<2                                              //
// which can be executed without problems.                                    //
// ************************************************************************** //


module CondStat3(nat i,[2]bool ?a,event !error) {
    i = 1;
    if(a[i-1]) emit(error);
}
drivenby {
    nothing;
}