Abstract interface

Solution of a reachability 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.


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

Solution of a verification problem

CheckSolution{T} <: AbstractSolution

Type that wraps the solution of a verification problem.




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.


Solving a reachability problem

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.


  • 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.


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


  • 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.


Solving a hybrid reachability problem

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

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


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


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.


TODO: document other methods in solutions.jl.