// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// In the module below, the value of the local variable "a" is not known.     //
// Thus, the conditional statement can neither execute its "then" nor its     //
// "else" branch. Even though the branches would both assign d the value 1,   //
// the program cannot be executed. The generated guarded actions are as       //
// follows:                                                                   //
//     a => a = True                                                          //
//    True => b = 1                                                           //
//    True => c = 1                                                           //
//     a => d = b                                                             //
//    !a => d = c                                                             //
// ************************************************************************** //


module CondStat4(nat b,c,d) {
    event a;
    if(a) emit(a);
    b = 1;
    c = 1;
    if(a) d = b;
    else d = c;
}
drivenby {
    nothing;
}