|type||# of discrete variables||# of clocks||# of rest variables||# of controller modes||# of plant modes||# of jumps|
|timed & discrete||9||1||2||8||3||34|
|Type||Continuous dynamics||Guards & Invariants||Resets|
|hybrid||constant||hyperplane & half-space||constant|
This benchmark models a water tank which leaks, i.e., it has a constant outflow. The tank can be refilled from an unlimited external resource with a constant inflow that is larger than the outflow. The PLC controller triggers refilling (by switching a pump on) if a sensor indicates a low water level (). If the water level is high () the controller stops refilling (switches the pump off). Adding the controller introduces two controller input variables for low and high water levels, variables for the actuator (pump) state in the plant and the controller, and a variable to store the controller mode. Furthermore, a new clock is added to model the PLC cycle time. Besides the controller we also model a user which can manually switch
the pump on and off as far as the water level allows it. In our implementation, the user constantly toggles between the pump states on and off. We analyse the system behaviour over a global time horizon of $40$ seconds using a PLC cycle time of $2$ seconds.
The dynamics of the waterlevel of the tank 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 HyPro.
 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).