// 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(); } } } }