backward

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

@@ -1,7 +1,9 @@
-# ==================================
-# Backward approximation
-# ==================================
+"""
+Backward approximation discretization algorithm.
+"""
+module BackwardModule
 
+using ..DiscretizationModule
 using ..Exponentiation: _alias
 
 """
@@ -57,3 +59,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,6 +2,8 @@
 # Discretize using the correction hull of the matrix exponential
 # ===============================================================
 
+using IntervalMatrices: correction_hull, input_correction
+
 using ..Exponentiation: _exp, _alias
 
 """

src/Discretization/DiscretizationModule.jl

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

src/Discretization/Forward.jl

@@ -94,10 +94,10 @@ function discretize(ivp::IVP{<:CLCS,Interval{N}}, δ, alg::Forward) where {N}
 
     # a_sqr = a * a
     #P2A_abs = (1/a_sqr) * (Φ - one(N) - aδ)
-    #Einit = (P2A_abs * a_sqr) * RA._symmetric_interval_hull(X0).dat
+    #Einit = (P2A_abs * a_sqr) * LazySets.symmetric_interval_hull(X0).dat
 
     #P2A_abs = (1/a_sqr) * (Φ - one(N) - aδ)
-    Einit = (Φ - one(N) - aδ) * convert(Interval, _symmetric_interval_hull(X0)).dat
+    Einit = (Φ - one(N) - aδ) * convert(Interval, LazySets.symmetric_interval_hull(X0)).dat
 
     Ω0 = Interval(hull(X0.dat, Φ * X0.dat + Einit))
     X = stateset(ivp)

src/Discretization/discretization.jl

@@ -1,105 +1,20 @@
-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 inteval 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 # TEMP
+using ..Exponentiation # TMP
 include("NoBloating.jl")
 
 # Forward approximation
 include("Forward.jl")
 
 # Backward approximation
-include("Backward.jl")
+include("BackwardModule.jl")
+using .BackwardModule
 
 # Intersect one step forward in time with one step backward
 include("StepIntersect.jl")

src/Flowpipes/setops.jl

@@ -364,19 +364,6 @@ function _split(A::IntervalMatrix{T,IT,MT}) where {T,IT,ST,MT<:StaticArray{ST,IT
     return SMatrix{m,n,T}(C), SMatrix{m,n,T}(S)
 end
 
-_symmetric_interval_hull(x::Interval) = LazySets.symmetric_interval_hull(x)
-_symmetric_interval_hull(x::Hyperrectangle) = LazySets.symmetric_interval_hull(x)
-
-# type-stable version
-function _symmetric_interval_hull(S::LazySet{N}) where {N}
-    # fallback returns a hyperrectangular set
-    (c, r) = box_approximation_helper(S)
-    #if r[1] < 0
-    #    return EmptySet{N}(dim(S))
-    #end
-    return Hyperrectangle(zeros(N, length(c)), abs.(c) .+ r)
-end
-
 # type-stable version
 function _overapproximate(S::LazySet{N}, ::Type{<:Hyperrectangle}) where {N}
     c, r = box_approximation_helper(S)