// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // This module demonstrates that one has to distinguish between the surface // // and the depth of statements: When resuming the execution from location w // // under the condition that i holds, the depth, i.e., emit(o2) has to be // // aborted, while the surface, i.e, emit(o1) is allowed to execute due to // // the delayed abortion. // // ************************************************************************** // module RedoAbort(event ?i,!o1,!o2) { loop abort { emit(o1); w: pause; emit(o2); } when(i); } satisfies { s1 : assert o1 & !o2; s3 : assert A X A G o1; s4 : assert A X A G (o2 <-> !i); } drivenby { pause; emit(i); }