|type||# of discrete variables||# of clocks||# of rest variables||# of controller modes||# of plant modes||# of jumps|
|timed & discrete||5||1||7||6||2||18|
|Type||Continuous dynamics||Guards & Invariants||Resets|
|hybrid||linear polynomial||hyperplane & half-space||constant|
In this benchmark a heater with a thermostat controller is modelled. Initially, the temperature is and the heater is on. The controller keeps the temperature between and . The heater is switched off if the temperature rises above and it is switched on at a
temperature below . Adding a controller to the model introduces new variables for the low and high temperature sensors in the controller, a variable for the actuator (heater) state in the plant and the controller, and a variable to store the controller mode. Additionally, we introduce a new clock for the cycle time of the PLC. The global time horizon is 10 seconds and the PLC cycle time is 0.5 seconds.
The dynamics of the temperature is defined by the following differential equations:
We consider an initial set of
and the starting location , a time horizon , a PLC cycle duration of , and a time step .
Fig.1 shows the flowpipes computed for the above-mentioned parameters using a) Hypro and b) SpaceEx.
 J. Nellen. Analysis and synthesis of hybrid systems in engineering applications. PhD Thesis, RWTH Aachen University, 2016.
 S. Schupp et al.. Divide and conquer: Variable set separation in hybrid systems reachability analysis. Submitted to (QAPL’17).