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