Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

backward module #753

Merged
merged 5 commits into from
Jan 14, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions docs/src/lib/discretize.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Depth = 3
## Discretize API

```@docs
ReachabilityAnalysis.DiscretizationModule
normalize
discretize
```
Expand Down
Original file line number Diff line number Diff line change
@@ -1,9 +1,13 @@
# ==================================
# Backward approximation
# ==================================
module BackwardModule

using ..DiscretizationModule
using ..Exponentiation: _alias

export Backward

"""
Backward{EM, SO, SI, IT, BT} <: AbstractApproximationModel

Expand Down Expand Up @@ -57,3 +61,5 @@ end
Base.show(io::IO, m::MIME"text/plain", alg::Backward) = print(io, alg)

# TODO: add corresponding `discrete` methods <<<<<

end
5 changes: 5 additions & 0 deletions src/Discretization/CorrectionHull.jl
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,12 @@
# Discretize using the correction hull of the matrix exponential
# ===============================================================

using Reexport

using IntervalMatrices: correction_hull, input_correction

using ..Exponentiation: _exp, _alias
@reexport import ..DiscretizationModule: discretize

"""
CorrectionHull{EM} <: AbstractApproximationModel
Expand Down
98 changes: 98 additions & 0 deletions src/Discretization/DiscretizationModule.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,98 @@
"""
Interface for conservative time discretization methods.
"""
module DiscretizationModule

using MathematicalSystems
import IntervalArithmetic as IA
using IntervalMatrices
using LazySets
using LazySets.Approximations: AbstractDirections
using Reexport

using ..Exponentiation
import ..Exponentiation: _alias

@reexport import MathematicalSystems: discretize
export AbstractApproximationModel, sih, isinterval

abstract type AbstractApproximationModel end

function _default_approximation_model(ivp::IVP{<:AbstractContinuousSystem})
return Forward()
end

# some algorithms require a polyhedral computations backend
hasbackend(alg::AbstractApproximationModel) = false

# symmetric interval hull options
sih(X, ::Val{:lazy}) = SymmetricIntervalHull(X)
sih(X, ::Val{:concrete}) = LazySets.symmetric_interval_hull(X)

# interval matrix functions
isinterval(A::AbstractMatrix{N}) where {N<:Number} = false
isinterval(A::IntervalMatrix{N,IT}) where {N,IT<:IA.Interval{N}} = true
isinterval(A::AbstractMatrix{IT}) where {IT<:IA.Interval} = true

# options for a-posteriori transformation of a discretized set
# valid options are:
# AbstractDirections, Val{:lazy}, Val{:concrete}, Val{:vrep}, Val{:zono}, Val{:zonotope}
# _alias(setops) = setops # no-op

_alias(setops::AbstractDirections) = setops
_alias(setops::Val{:lazy}) = setops
_alias(setops::Val{:concrete}) = setops
_alias(setops::Val{:vrep}) = setops
_alias(setops::Val{:box}) = setops
_alias(setops::Val{:zono}) = setops
_alias(setops::Val{:zonotope}) = Val(:zono)

"""
discretize(ivp::IVP, δ, alg::AbstractApproximationModel)

Set-based conservative discretization of a continuous-time initial value problem
into a discrete-time problem.

### Input

- `ivp` -- initial value problem for a linear ODE in canonical form (see `Notes` below)
- `δ` -- step size
- `alg` -- algorithm used to compute the approximation model

### Output

The initial value problem of a discrete system.

### Notes

Different approximation algorithms and their respective options are described
in the docstring of each method. Here is a list of all the available approximation models:

```jldoctest
julia> subtypes(ReachabilityAnalysis.AbstractApproximationModel)
5-element Vector{Any}:
Backward
CorrectionHull
Forward
NoBloating
StepIntersect
```

Initial-value problems considered in this function are of the form

```math
x' = Ax(t) + u(t),\\qquad x(0) ∈ \\mathcal{X}_0,\\qquad (1)
```
and where ``u(t) ∈ U(k)`` add where ``\\{U(k)\\}_k`` is a sequence of sets of
non-deterministic inputs and ``\\mathcal{X}_0`` is the set of initial
states. Other problems, e.g. ``x' = Ax(t) + Bu(t)`` can be brought
to the canonical form with the function [`normalize`](@ref).

For references to the original papers introducing each algorithm, see the docstrings,
e.g. `?Forward`.
"""
function discretize(ivp::IVP, δ, alg::AbstractApproximationModel)
return error("discretization not implemented for the given arguments: $ivp, $alg")
end

end
4 changes: 4 additions & 0 deletions src/Discretization/FirstOrder.jl
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,12 @@
# First-order approximation model
# ===============================

using Reexport

using ..Exponentiation: _exp

@reexport import ..DiscretizationModule: discretize

"""
FirstOrder{EM} <: AbstractApproximationModel

Expand Down
4 changes: 4 additions & 0 deletions src/Discretization/FirstOrderZonotope.jl
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,10 @@
# First-order approximation model with zonotopes
# ==============================================

using Reexport

@reexport import ..DiscretizationModule: discretize

"""
FirstOrderZonotope{EM} <: AbstractApproximationModel

Expand Down
4 changes: 4 additions & 0 deletions src/Discretization/Forward.jl
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,12 @@
# Forward approximation
# ==================================

using Reexport

using ..Exponentiation: _exp, _alias

@reexport import ..DiscretizationModule: discretize

"""
Forward{EM, SO, SI, IT, BT} <: AbstractApproximationModel

Expand Down
3 changes: 3 additions & 0 deletions src/Discretization/ForwardBackward.jl
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
using Reexport

using ..Exponentiation: _exp, _alias
@reexport import ..DiscretizationModule: discretize

# obs: S should normally be <:JuMP.MOI.AbstractOptimizer
struct ForwardBackward{EM,SO,SI,IT,BT,S} <: AbstractApproximationModel
Expand Down
4 changes: 4 additions & 0 deletions src/Discretization/NoBloating.jl
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,12 @@
# Approximation model in discrete time, i.e. without bloating
# ============================================================

using Reexport

using ..Exponentiation: _exp, _alias

@reexport import ..DiscretizationModule: discretize

"""
NoBloating{EM, SO, IT} <: AbstractApproximationModel

Expand Down
3 changes: 3 additions & 0 deletions src/Discretization/SecondOrderddt.jl
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,10 @@
# Second-order approximation from d/dt
# ===================================

using Reexport

using ..Exponentiation: _exp, _alias
@reexport import ..DiscretizationModule: discretize

"""
SecondOrderddt{EM, SO, SI, IT, BT} <: AbstractApproximationModel
Expand Down
4 changes: 4 additions & 0 deletions src/Discretization/StepIntersect.jl
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,12 @@
# backward of the same model
# ============================================================================

using Reexport

using ..Exponentiation: _exp, _alias

@reexport import ..DiscretizationModule: discretize

"""
StepIntersect{DM<:AbstractApproximationModel} <: AbstractApproximationModel

Expand Down
98 changes: 7 additions & 91 deletions src/Discretization/discretization.jl
Original file line number Diff line number Diff line change
@@ -1,105 +1,21 @@
using IntervalMatrices: correction_hull, input_correction
using Reexport

using .Exponentiation
import ..Exponentiation: _alias

# ==================================
# Abstract interface
# ==================================

abstract type AbstractApproximationModel end

function _default_approximation_model(ivp::IVP{<:AbstractContinuousSystem})
return Forward()
end

# some algorithms require a polyhedral computations backend
hasbackend(alg::AbstractApproximationModel) = false

# symmetric interval hull options
sih(X, ::Val{:lazy}) = SymmetricIntervalHull(X)
sih(X, ::Val{:concrete}) = symmetric_interval_hull(X)

# interval matrix functions
isinterval(A::AbstractMatrix{N}) where {N<:Number} = false
isinterval(A::IntervalMatrix{N,IT}) where {N,IT<:IA.Interval{N}} = true
isinterval(A::AbstractMatrix{IT}) where {IT<:IA.Interval} = true

# options for a-posteriori transformation of a discretized set
# valid options are:
# AbstractDirections, Val{:lazy}, Val{:concrete}, Val{:vrep}, Val{:zono}, Val{:zonotope}
# _alias(setops) = setops # no-op

_alias(setops::AbstractDirections) = setops
_alias(setops::Val{:lazy}) = setops
_alias(setops::Val{:concrete}) = setops
_alias(setops::Val{:vrep}) = setops
_alias(setops::Val{:box}) = setops
_alias(setops::Val{:zono}) = setops
_alias(setops::Val{:zonotope}) = Val(:zono)

"""
discretize(ivp::IVP, δ, alg::AbstractApproximationModel)

Set-based conservative discretization of a continuous-time initial value problem
into a discrete-time problem.

### Input

- `ivp` -- initial value problem for a linear ODE in canonical form (see `Notes` below)
- `δ` -- step size
- `alg` -- algorithm used to compute the approximation model

### Output

The initial value problem of a discrete system.

### Notes

Different approximation algorithms and their respective options are described
in the docstring of each method, e.g. [`Forward`](@ref). Here is a list of all
the available approximation models:

```jldoctest
julia> subtypes(ReachabilityAnalysis.AbstractApproximationModel)
5-element Vector{Any}:
Backward
CorrectionHull
Forward
NoBloating
StepIntersect
```

Initial-value problems considered in this function are of the form

```math
x' = Ax(t) + u(t),\\qquad x(0) ∈ \\mathcal{X}_0,\\qquad (1)
```
and where ``u(t) ∈ U(k)`` add where ``\\{U(k)\\}_k`` is a sequence of sets of
non-deterministic inputs and ``\\mathcal{X}_0`` is the set of initial
states. Other problems, e.g. ``x' = Ax(t) + Bu(t)`` can be brought
to the canonical form with the function [`normalize`](@ref).

For references to the original papers introducing each algorithm, see the docstrings,
e.g. `?Forward`.
"""
function discretize(ivp::IVP, δ, alg::AbstractApproximationModel)
return error("discretization not implemented for the given arguments: $ivp, $alg")
end

# =========================================
# Conservative time discretization methods
# =========================================

using Reexport
include("DiscretizationModule.jl")

# Approximation model in discrete time, i.e. without bloating
using ..DiscretizationModule # TODO Remove
using ..Exponentiation # TODO Remove
include("NoBloating.jl")

# Forward approximation
include("Forward.jl")

# Backward approximation
include("Backward.jl")
include("BackwardModule.jl")
@reexport using ..BackwardModule

# Intersect one step forward in time with one step backward
include("StepIntersect.jl")
Expand Down
1 change: 0 additions & 1 deletion src/Initialization/exports.jl
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ export
CorrectionHull,
FirstOrder,
ForwardBackward,
#Backward,
Forward,
NoBloating,
StepIntersect,
Expand Down
Loading