// ************************************************************************** //
//                                                                            //
//    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 module is in analogy to CondStat0 (which should be read first). It    //
// behaves different to CondStat0, since it generates the following guarded   //
// actions:                                                                   //
//  * True => error = 0<i&0<i-1                                               //
//  * True => assert 1<=i                                                     //
// Since initially i==0 holds, the expression 0<i&0<i-1 evaluates to false    //
// since (false&top is false), but the assertion fails.                       //
// See also CondStat0.qrz for comparison.                                     //
// ************************************************************************** //


module CondExpr0(nat ?i,event !error) {
    error = (i>0 ? (i-1>0) : false );
}
drivenby {
    nothing;
}