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:
