## Classification

# of variables | # of modes | # of jumps |
---|---|---|

3 | 2 | 2 |

Type | Continuous dynamics | Guards & Invariants | Resets |
---|---|---|---|

hybrid | linear polynomial | hyperplane & half-space | constant |

## Download

Flow* | rod_reactor1.zip |

SpaceEx | rod_reactor.zip |

## Model description

This benchmark consists of a reactor tank and two independent rods. The goal is to control the coolant temperature in the tank by putting in or taking out the rods [1]. The rods differ in their cooling dynamics. Two clocks are introduced to measure the time elapsed since the last use

of respectively rod1 and rod2.

The hybrid automaton of the benchmark:

## Reachability settings

The initial set is:

The initial location is the location “No Rods” and the time horizon . The set of unreachable states are all states in location .

## Results

The state shutdown is not reachable. The following plots are taken from SpaceEx: