// ************************************************************************** //
//                                                                            //
//    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 extends the discussion of the semantics of conditional    //
// statements and expressions. It shows the behavior of conditionals whose    //
// conditions evaluate to TOP. The module has semantic problems, which is     //
// seen by its generated guarded actions:                                     //
//    True => b = 1                                                           //
//    True => c = 1                                                           //
//    True => d = 1==5/a?b:c                                                  //
//    True => assert !(a==0)                                                  //
// Indeed, the fixpoint iteration yields an environment with a==0, since      //
// the reaction to absence assigns this value to a. Thus, the assertion fails.//
// ************************************************************************** //


module CondExpr5(nat b,c,d) {
    nat a;
    b = 1;
    c = 1;
    d = (5/a==1?b:c);
}
drivenby {
    nothing;
}