# Solutions

## Abstract interface

`ReachabilityAnalysis.AbstractSolution`

— Type`AbstractSolution`

Abstract supertype of all solution types of a rechability problem.

## Solution of a reachability problem

`ReachabilityAnalysis.ReachSolution`

— Type`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`AbstractReachSet`

s`alg`

– algorithm used`options`

– the dictionary of options

## Solution of a verification problem

`ReachabilityAnalysis.CheckSolution`

— Type`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.

## Solving a reachability problem

`CommonSolve.solve`

— Function`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.

`ReachabilityAnalysis.AbstractPost`

— Type`AbstractPost`

Abstract supertype of all post operator types.

`ReachabilityAnalysis.AbstractContinuousPost`

— Type`AbstractContinuousPost`

Abstract supertype of all continuous post operators.

`ReachabilityAnalysis.AbstractDiscretePost`

— Type`AbstractDiscretePost`

Abstract supertype of all discrete post operators.

## Solving a hybrid reachability problem

`ReachabilityAnalysis.AbstractWaitingList`

— Type`AbstractWaitingList`

Abstract supertype for all waiting list types.

`ReachabilityAnalysis.WaitingList`

— Type`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.

`ReachabilityAnalysis.StateInLocation`

— Type`StateInLocation{ST,M}`

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

TODO: document other methods in `solutions.jl`

.