// ************************************************************************** //
//                                                                            //
//    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);
}