Merge pull request #753 from JuliaReach/mforets/backward

backward module

docs/src/lib/discretize.md

@@ -13,6 +13,7 @@ Depth = 3
 ## Discretize API
 
 ```@docs
+ReachabilityAnalysis.DiscretizationModule
 normalize
 discretize
 ```

src/Discretization/Backward.jl → src/Discretization/BackwardModule.jl

@@ -1,9 +1,13 @@
 # ==================================
 # Backward approximation
 # ==================================
+module BackwardModule
 
+using ..DiscretizationModule
 using ..Exponentiation: _alias
 
+export Backward
+
 """
     Backward{EM, SO, SI, IT, BT} <: AbstractApproximationModel
 
@@ -57,3 +61,5 @@ end
 Base.show(io::IO, m::MIME"text/plain", alg::Backward) = print(io, alg)
 
 # TODO: add corresponding `discrete` methods <<<<<
+
+end

src/Discretization/CorrectionHull.jl

@@ -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

src/Discretization/DiscretizationModule.jl

@@ -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

src/Discretization/FirstOrder.jl

@@ -2,8 +2,12 @@
 # First-order approximation model
 # ===============================
 
+using Reexport
+
 using ..Exponentiation: _exp
 
+@reexport import ..DiscretizationModule: discretize
+
 """
     FirstOrder{EM} <: AbstractApproximationModel
 

src/Discretization/FirstOrderZonotope.jl

@@ -2,6 +2,10 @@
 # First-order approximation model with zonotopes
 # ==============================================
 
+using Reexport
+
+@reexport import ..DiscretizationModule: discretize
+
 """
     FirstOrderZonotope{EM} <: AbstractApproximationModel
 

src/Discretization/Forward.jl

@@ -2,8 +2,12 @@
 # Forward approximation
 # ==================================
 
+using Reexport
+
 using ..Exponentiation: _exp, _alias
 
+@reexport import ..DiscretizationModule: discretize
+
 """
     Forward{EM, SO, SI, IT, BT} <: AbstractApproximationModel
 

src/Discretization/ForwardBackward.jl

@@ -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

src/Discretization/NoBloating.jl

@@ -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
 

src/Discretization/SecondOrderddt.jl

@@ -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

src/Discretization/StepIntersect.jl

@@ -3,8 +3,12 @@
 # backward of the same model
 # ============================================================================
 
+using Reexport
+
 using ..Exponentiation: _exp, _alias
 
+@reexport import ..DiscretizationModule: discretize
+
 """
     StepIntersect{DM<:AbstractApproximationModel} <: AbstractApproximationModel
 

src/Discretization/discretization.jl

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

src/Initialization/exports.jl

@@ -29,7 +29,6 @@ export
       CorrectionHull,
       FirstOrder,
       ForwardBackward,
-#Backward,
       Forward,
       NoBloating,
       StepIntersect,