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