Solutions

AbstractSolution

Abstract supertype of all solution types of a rechability problem.

ReachSolution{FT<:AbstractFlowpipe, ST<:AbstractPost} <: AbstractSolution

Type that wraps the solution of a reachability problem as a sequence of lazy sets, and a dictionary of options.

Fields

• Xk – the list of AbstractReachSets
• alg – algorithm used
• options – the dictionary of options

CheckSolution{T} <: AbstractSolution

Type that wraps the solution of a verification problem.

Fields

TODO

Notes

This type contains the answer if the property is satisfied, and if not, it contains the index at which the property might be violated for the first time.

solve(ivp::IVP{<:AbstractContinuousSystem}, tspan, alg; kwargs...)

Solves the initial-value problem defined by ivp over the time span tspan, using the algorithm alg. If no algorithm is given, a default algorithm is chosen.

Input

• ivp – initial-value problem
• tspan – time span for this initial-value problem
• alg – reachability algorithm

Additional options are passed as arguments or keyword arguments; see the notes below for details. See the online documentation for examples.

Output

The solution of a reachability problem, as an instance of a ReachSolution.

Notes

• Use the alg, algorithm or opC keyword arguments to specify the algorithm to solve the initial-value problem. Algorithm-specific options should be passed to the algorithm constructor as well.

• Use the tspan keyword argument to specify the time span; it can be:

  • a tuple,
  • an interval, or
  • a vector with two components.

• Use the T keyword argument to specify the time horizon; the initial time is then assumed to be zero.

• Use the static keyword argument to force conversion to static arrays in the algorithm (should be supported by the algorithm).

• Use the NSTEPS keyword argument to specify the number of discrete steps solved in the set-based recurrence.

• Use the threading option to use multi-threading parallelism. This option applies for initial-value problems whose initial condition is a vector of sets.

AbstractPost

Abstract supertype of all post operator types.

AbstractContinuousPost

Abstract supertype of all continuous post operators.

AbstractDiscretePost

Abstract supertype of all discrete post operators.

AbstractWaitingList

Abstract supertype for all waiting list types.

WaitingList{TN, ST, M, QT<:StateInLocation{ST, M}} <: AbstractWaitingList

Iterable container representing a list of pairs (set, mode) of a hybrid automaton.

Fields

• times – vector with a time interval associated to each state
• array – vector of StateInLocation

Notes

A WaitingList is a list of pairs `(set_i, loc_i) for i in 1..k where times is a vector with a time interval associated to each state.

This waiting list allows for a unique set representation (ST) for all elements of the list.

StateInLocation{ST,M}

Struct that associates a set with a hybrid automaton's location index, usually an integer.