We study the behavior of the planar spring-pendulum described in . It consists of a solid ball of mass and a spring of natural length . The spring constant is .
We study the evolutions of the length of the spring and the angle between the spring and the vertical. They are modeled by the following differential equations
which can be equivalently translated to the first-order ODE as below.
The constants are set as , , and .
We consider the initial set , , and .
The following figure shows an overapproximation computed by Flow* for the time horizon .