Chapter 3
The Input

The following is an example input file:

VARIABLES [ x, y ]  
MODES [ m1 ]  
  m1[[0, 4], [0, 4]]  

As can be seen, the input allows several keywords followed by additional information. The keywords are:

The constraints should be formulated in the syntax of RSolver . More example inputs are contained in the distribution package.

Throughout, the input allows comments in the form (* comment *).

For debugging syntax errors, it may help to produce a parser trace by setting the Shell environment variable OCAMLRUNPARAM to p (for example, in Bash, using export OCAMLRUNPARAM=p).

Note that the formalism allows the modeling of invariants using constraints on the state space variables in the FLOW and JUMP sections. When doing so, the start- and the endpoint of a jump should satisfy the invariant of the source and the target mode, respectively. For example, an invariant x < 1 in mode m1 and x 1 in mode m2 does not allow jumps from mode m1 to mode m2 that leave x unchanged. If such jumps are intended, the invariant of mode m1 should be x 1.

Note also that the conditions for jumping from a mode m1 to a mode m2 should be well-separated from the conditions for jumping back from mode m2 to m1. For example, in the case when a hybrid system uses dynamics = f1(x) whenever x < 0 and = f2(x) whenever x 0, this should be modeled using a jump from a mode with dynamics f1 to a mode with dynamics f2 for x > ε, and a jump back for x ≤-ε. This takes into account switching delays occurring in actual system implementations, and avoids infinite loops between the two modes.