|# of variables||# of modes||# of jumps|
|Type||Continuous dynamics||Guards & Invariants||Resets|
|hybrid||linear polynomial||hyperplane & half-space||constant|
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 . 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:
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 .
The state shutdown is not reachable. The following plots are taken from SpaceEx: