  Hybrid systems can express a plethora of physical phenomena and systems as
they can combine continuous and discrete dynamics. There exist several tools
that enable the reachability analysis of hybrid systems modeled as hybrid
automata. However, these tools exhibit certain limitations in the type of
mathematical operations that they natively support. For example, SpaceEx, a
well-established tool in the hybrid verification community, supports the use of
linear ODEs in the flow of each discrete location. Mathematical functions like
algebraic equations or trigonometric functions have to be encoded as the
solutions of a set of ODEs. In this article, we provide a mechanism to define
sinusoidal functions that are supported by SpaceEx. We also show how certain
Simulink blocks can be translated into hybrid automata.
