Rod reactor


# of variables # of modes # of jumps
3 2 2
Type Continuous dynamics Guards & Invariants Resets
hybrid linear polynomial hyperplane & half-space constant



Model description

This benchmark consists of a reactor tank and two independent rods. The goal is to control the coolant temperature x in the tank by putting in or taking out the rods [1]. The rods differ in their cooling dynamics. Two clocks c_1, c_2 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:

  • x=510
  •  c1,c2=20

The initial location is the location “No Rods” and the time horizon T=50 sec. The set of unreachable states are all states in location shut~down.


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


[1] F. Vaandrager. Lecture notes: Hybrid Systems.