// ============================================================================
// Name:        ABRO1
// Description: Generic version of the ABRO example. Wait on the signals
//              a[0..EVENTS] and emit the output o. Restart each time the
//              reset signal r occurs.
// References:  http://www.esterel-technologies.com/files/primer.zip
// Parameters:  EVENTS (number of events)
// ============================================================================

#ifndef EVENTS
#define EVENTS 2
#endif

module ABRO1(bool a[EVENTS], event r, &o) implements ABRO1Spec(a, r, o) {
   loop
      abort {
         parallel(int[sizeOf(EVENTS-1)] i=0 .. (EVENTS-1))
            await(a[i]);
         emit o;
         await(r);
      } when(r);
}

spec ABRO1Spec(bool a[EVENTS], event r, o) {
   S1: A G (o -> exists(int[sizeOf(EVENTS-1)] i=0 .. (EVENTS-1)) a[i]);
   S2: A G (o -> forall(int[sizeOf(EVENTS-1)] i=0 .. (EVENTS-1)) [a[i] PWB r]);
   S3: A G (o -> A X !o);
}