// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // Simple version of the ABRO example. The program waits on the signals a and // // b in parallel, and emits the output o as soon as that last of the signals // // becomes true. The behavior is restarted if the reset signal is true. // // ************************************************************************** // module ABRO(event ?a,?b,?r,!o) { loop abort { {wa: await(a); || wb: await(b);} emit(o); wr: await(r); } when(r); } satisfies { property0: assert A G (o -> a); property1: assert A G (o -> a | b); property2: assert A G (o -> [a PWB r] & [b PWB r]); property3: assert A G (o -> A X !o); } drivenby { pause; emit(a); pause; emit(r); pause; emit(a); pause; emit(b); pause; emit(a); pause; emit(r); pause; }