// ************************************************************************** // // // // 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 is a generic version of the ABRO example. The module waits on the // // signals a[...] and emits the output o as soon as the last of the signals // // a[i] arrives. After that, an occurrence of signal r is awaited to restart // // the behavior. In contrast to ABRO1, the behavior immediately restarts when // // the emission is made (without waiting for r). // // ************************************************************************** // macro Events = 4; module ABRO3(event [Events]bool ?a, event ?r, !o) { loop abort { for(i=0 .. (Events-1)) do || await(a[i]); emit(o); } when(r); } satisfies { property1 : assert A G (o -> exists(i=0 .. (Events-1)) a[i]); property2 : assert A G (o -> forall(i=0 .. (Events-1)) [a[i] PWB r]); }