// ************************************************************************** // // // // 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). In contrast to ABRO1, the // // emission of signal o is delayed. // // ************************************************************************** // macro Events = 4; module ABRO2(event [Events]bool ?a,event ?r,!o) { loop abort { for(i=0 .. (Events-1)) do || await(a[i]); emit next(o); await(r); } when(r); } satisfies { S1 : assert A G (o -> PSX exists(i=0 .. (Events-1)) a[i]); S2 : assert A G (o -> PSX forall(i=0 .. (Events-1)) [a[i] PWB r]); S3 : assert A G (o -> A X !o); }