Filtered oscillator


# of variables # of modes # of jumps
6-34 4 4
Type Continuous dynamics Guards & Invariants Resets
hybrid linear polynomial hyperplane & half-space identity


Flow* filtered_oscillator_4, filtered_oscillator_8filtered_oscillator_16filtered_oscillator_32
SpaceEx filtered_oscillator_4, filtered_oscillator_8, filtered_oscillator_16, filtered_oscillator_32

Model description

This benchmark consists of a two-dimensional switched oscillator (variables x,y) plus an 4-th order filter with state variables x1,x2,x3, and z. The filter smoothens the signal x and has z as the output signal. At the switching planes (diagonal and horizontal in the x/y-plane) the system changes the discrete state, but does not modify the variables. Similar to the circle example, this illustrates the two sources of overapproximation: The overapproximation of the continuous trajectory in each quadrant, and the overapproximation resulting from the change of discrete state. In this example, the flowpipes hit the diagonal switching plane at an angle, such that many convex sets intersect with the plane and can take the transition. To reduce the number of sets, groups of them are clustered by taking their template hull. The preset clustering percentage for this example is 100, so all sets are clustered into a single convex set. Reduce the percentage to see more sets and flowpipes generated. In addition, try aggregating the clusters into a single convex set by changing the set-aggregation option to convex hull. This generates a single set, but being the convex hull of the clusters this can be significantly more precise than the template hull produced by clustering into a single set.


Reachability settings

We use as the initial set:

  •  x \in [0.2,0.3]
  •  y \in [-0.1,0.1]
  • z,x_1,x_2,x_3=0

We consider a time horizon T=4 and the bad states are the states where y \geq 0.5.


filtered_oscillator_4_3 filtered_oscillator_4_2 filtered_oscillator_4_1