// Commentary:
//
// This is an erroneous example of a cruise control system.  Usually a
// cruise control system centers around the PID feedback control loop,
// where functional requirements like reaching and maintaining the set
// velocity comfortably, i.e. with the proper stability and
// responsiveness.  Here we abstract away from those specific
// requirements and focus on the interactions between the different
// actors in the system represented as the HMI, the pedals and the
// throttle actuator.
//
// Note that the throttle actuator can be viewed as representing the
// actual PID control loop.
//
// This model can demonstrates a safety related functional error where
// the cruise control will continue to control the throttle after
// engaging the pedals, by forgetting to cancel the timer on line 103.
// In order to catch this error during verification line 92 must be
// enabled.
//
// Also note the increased number of states and transitions in the state
// diagram compared to the correct version.
//
// Code:

import ../cruise-control-interfaces.dzn;

component cruise_control
{
  provides ihmi hmi;
  requires ipedals pedals;
  requires ithrottle throttle;
  requires itimer timer;

  behavior
  {
    bool error = false;
    [hmi.state.Disabled] {
      on hmi.enable():
      {
        bool ignore = pedals.enable();
      }
      on hmi.disable(): {}
    }
    [!hmi.state.Disabled] {
      on hmi.enable(): {}
      on hmi.disable(): {
        throttle.reset();
        timer.cancel();
        pedals.disable();
      }
    }
    [hmi.state.Enabled && timer.idle] {
      [pedals.engaged] on hmi.set(): {/* ignore */}
      [!pedals.engaged] on hmi.set(): {
        if(!pedals.engaged) {
          throttle.set();
          timer.start();
        }
      }
      on hmi.resume(): {
        [pedals.engaged || !hmi.setpoint.Set] {/* ignore */}
        [otherwise] {
          throttle.set();
          timer.start();
        }
      }
    }
    [!hmi.state.Enabled || !timer.idle] {
      on hmi.set(): {}
      on hmi.resume(): {}
    }
    //[hmi.state.Active]
    on timer.timeout(): {
      throttle.set();
    }
    on hmi.cancel(): {
      throttle.reset();
      timer.cancel();
    }
    on pedals.engage()
      , throttle.unset(): {
      if(hmi.state.Active) hmi.inactive();
      throttle.reset();
      //timer.cancel();
    }
    on pedals.disengage(): {
      if(hmi.state.Active) {
        hmi.inactive();
      }
    }
  }
}