// ************************************************************************** // // // // 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 weak immediate variant is consistent and has the behavior specified // // with the given assertions. // // ************************************************************************** // module TrapVsWeakImmediateAbort(event a1,b1,a2,b2) { event t; weak immediate abort { emit(a1); emit(t); emit(b1); assert(a1 & t & b1 & !a2 & !b2); w: pause; emit(a2); emit(t); emit(b2); } when(t); assert(a1 & t & b1 & !a2 & !b2); } drivenby { pause; }