// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// A very simple cruise control system due to S. Ramesh.                      //
// Reference: H. Gomaa, Software Design Methods for Concurrent and Real-Time  //
// Systems, Addison-Wesley Publisher Co., 1993                                //
// ************************************************************************** //

package CruiseControl;


module CruiseControl(
    event
        ?ignitionOn, !chkBelts, !startEngine, ?engineOff,
        ?beltFastened, ?beltUnfastened, !alarm,
        ?cruise, ?accel, ?accelReleased, ?brakePressed,
        !cruising,
    int
        ?currentSpeed, !controlThrottle
) {
    loop {
        await (ignitionOn);
        emit (chkBelts);
        await (beltFastened);
        emit (startEngine);
        abort {
                loop {
                    abort
                        ManualMode(accelReleased,accel,controlThrottle);
                    when (cruise);
                    abort
                        CruiseMode(currentSpeed,controlThrottle,cruising);
                    when(brakePressed);
                }
            ||
                every (beltUnfastened)
                    emit (alarm);
        } when (engineOff);
    }
}