Leaking tank with controller


type # of discrete variables # of clocks # of rest variables # of controller modes # of plant modes # of jumps
original 0 0 12 8 3 34
timed 0 1 11 8 3 34
discrete 9 0 3 8 3 34
timed & discrete 9 1 2 8 3 34
Type Continuous dynamics Guards & Invariants Resets
hybrid constant hyperplane & half-space constant


SpaceEx spaceEx_files
HyPro hypro_files

Model description

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 ($h\leq 6$). If the water level is high ($h \geq 12$) 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:

    \[\dot{h} = \left\{ \begin{array}{l l} $\phantom{-}2$ & \quad \text{if the pump is on and the tank is not full}\\ $\phantom{-}2$ & \quad \text{if the tank is full}\\ $-1.5$ & \quad \text{if the pump is off}\\ \end{array} \right. \]

Reachability settings

We consider an initial set of

  • h = 10
  • \text{low} = 1
  • \text{high} = 0
  • P = P\_{\text{plc}} = 1
  • P\_{\text{on}} = P\_{\text{on}}\_{\text{plc}} = 0
  • P\_{\text{off}} = P\_{\text{off}}\_{\text{plc}} = 1
  • \text{nextSfcLoc} = 1
  • \text{cycle\_time} = 0
  • \text{global\_time} = 0

and the starting location \text{clock\_\_switch\_on\_in\_\_comm}, a time horizon $\text{global\_time}=40s$, a PLC cycle duration of $\delta = 2s$, and a time step $r=0.01s$ .


Fig.1 shows the flowpipes computed for the above-mentioned parameters using HyPro.

Figure 1: Flowpipe of the leaking tank system with controller


[1] J. Nellen. Analysis and synthesis of hybrid systems in engineering applications. PhD Thesis, RWTH Aachen University, 2016.

[2] S. Schupp et al.. Divide and conquer: Variable set separation in hybrid systems reachability analysis. Submitted to (QAPL’17).