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

module Z01(event bool ?a,?b,?c,o1,o2) {
    loop {
        abort {
            loop {
                emit(o1);
                l1: pause;
            }
        } when(a&b);
        ||
        {
            l2: pause;
            if(o1 & (a|c)) {
                emit(o2);
                l3: await(a);
            }
        }
    }
} drivenby {
    /* step 0 */
    emit(a);
    emit(b);
    emit(c);
    pause;
    /* step 1 */
    emit(a);
    emit(c);
    pause;
    /* step 2 */
    emit(c);
    pause;
    /* step 3 */
    emit(b);
    emit(a);
    pause;
    /* step 4 */
    emit(a);
    emit(b);   
}


//    The simulator stops in step 4 yielding the following incomplete environment:
//        a : True
//        b : True
//        c : False
//        o1 : ⊥
//        o2 : ⊥
//        l1 : True
//        l2 : True
//        l3 : False
//    
//    To give a first explanation, what the problem is, consider the generated guarded 
//    actions:
//        * l1&!(a&b) => o1 = True
//        * l1&a&b&(l3|l2&!o1) => o1 = True
//        * !l1&(a&l3 | l2&!(o1&(a|c))) => o1 = True
//        * !(l2|l3)&l1&a&b => o1 = True
//        * l2&o1&(a|c) => o2 = True
//    
//    Using the determined values of step 4, the following is left:
//        * !o1 => o1 = True
//        *  o1 => o2 = True
//    
//    This is a classic causality problem, since none of the actions must be executed,
//    and we cannot exclude them either, since by suitable values of o1 they could be
//    executed. If o1=True would hold, then only "o2 = True" must be executed, and 
//    therefore we have no emission of o1, which contradicts the assumption o1=True.
//    If o1=False would hold, "o1 = True" would be executed, which would also contradict
//    this assumption.
//