Skip to content

Commit

Permalink
make BackwardModule
Browse files Browse the repository at this point in the history
  • Loading branch information
Marcelo Forets committed Dec 3, 2023
1 parent 2bcb744 commit 20c9963
Show file tree
Hide file tree
Showing 4 changed files with 108 additions and 91 deletions.
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
# ==================================
# Backward approximation
# ==================================
module BackwardModule

using ..DiscretizationModule
using ..Exponentiation: _alias

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

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

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

using IntervalMatrices: correction_hull, input_correction

using ..Exponentiation: _exp, _alias

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

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

using ..Exponentiation
import ..Exponentiation: _alias

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 inteval 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, 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

end
96 changes: 5 additions & 91 deletions src/Discretization/discretization.jl
Original file line number Diff line number Diff line change
@@ -1,105 +1,19 @@
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
# =========================================

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")

# Intersect one step forward in time with one step backward
include("StepIntersect.jl")
Expand Down

0 comments on commit 20c9963

Please sign in to comment.