Chapter 3
The Input

The following is an example input file:

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

• VARIABLES: a list of the names of the variables spanning the continuous state space
• MODES: a list of the names of the discrete modes
• STATESPACE: for each mode, the hyper-rectangle spanning the corresponding continuous state space
• INITIAL: for each mode, a constraint describing the set of initial states in this mode
• FLOW: For each mode, some constraints restricting the possible flow in this mode:
  • In braces, for each state space variable, a constraint describing the continuous evolution of this variable. The i-th constraint may contain the variables as specified using the keyword VARIABLES, and the i-th variable followed by _d. The latter represents the derivative of this variable.
  • For linear differential equations, it is also possible to specify some eigenvalue and eigenvector related information here [2, 4] (for left eigenvalues λ an orthonormal basis of {c : A^T c = λc}, and for factors of the form y²+ay+b of the left characteristic polynomial an orthonormal basis of {c : ((A^T )² - 2aA^T + (a² + b²)I)c = 0}). This will provide the solver with additional optimization possibilities. Some examples of input files using this feature can be found in the distribution.
  • Delimited by {| and |} one can specify a constraint that specifies the possible flows explicitly (i.e., as a function of time instead of a differential equation). In addition to the state space variables, this constraint may contain the state space variables with the additional postfix _s, and the time variable t. It specifies that a flow taking time t is possible starting from the variables with the postfix _s to the variables without postfix.

  Note that the notion of ”trajectory” is defined in such a way that along flows, such a trajectory has to be differentiable. Hence one cannot use the constraints under the keyword FLOW to specificy non-differentiable evolution, for example, the specification of trajectories that change from following one differential equation to a different one.

• JUMP: for each pair of modes, a constraint describing discontinuous jumps of trajectories. For example, we use the string m1- > m2{x = 1 ∧ y = 2 ∧ x′ = 3 ∧ y′ = 5} for a jump from mode m₁ to mode m₂. The constraint may contain the variables as specified using the keyword VARIABLES, and their primed versions. The unprimed versions describe the jump source and the primed versions the jump target. Jumps may occur between all pairs of states that are solutions of this constraint.
• UNSAFE: for each mode, a constraint describing the set of unsafe states in this mode

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 ẋ = f₁(x) whenever x < 0 and ẋ = f₂(x) whenever x ≥ 0, this should be modeled using a jump from a mode with dynamics f₁ to a mode with dynamics f₂ 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.