// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// Measure the speed of a vehicle by counting the number of centimeters taken //
// within every second. Note the the speed remains constant until a new event //
// on second occurs. The example is taken from the Esterel primer.            //
// This version is a correct and has the following guarded actions:           //
//                                                                            //
//    <!second ==> next(s0) = true>                                           //
//    < second ==> next(s0) = true>                                           //
//    <cm&!second ==> next(dist) = dist+1>                                    //
//    <cm& second ==> next(dist) = dist@1+1>                                  //
//    <second ==> dist@1 = 0>                                                 //
//    <second ==> speed = dist>                                               //
//                                                                            //
// ************************************************************************** //

module Speed(event ?cm,?second,nat !speed) {
    loop {
        weak abort {
            nat dist;
            dist = 0;
            if(cm) next(dist) = dist+1;
            do {
                s0:pause;
                if(cm) next(dist) = dist+1;
            } while(!second);
            speed = dist;
        } when(second);
    }
}