#507 - Remove invariant argument from post

src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl

@@ -235,18 +235,17 @@ function init!(𝒫::BFFPSV18, 𝑆::AbstractSystem, 𝑂::Options)
 end
 
 """
-    post(𝒫::BFFPSV18, 𝑆::AbstractSystem, invariant, 𝑂::Options)
+    post(𝒫::BFFPSV18, 𝑆::AbstractSystem, 𝑂::Options)
 
 Calculate the reachable states of the given initial value problem using `BFFPSV18`.
 
 ### Input
 
 - `𝒫` -- post operator of type `BFFPSV18`
 - `𝑆` -- sytem, initial value problem for a continuous ODE
-- `invariant` -- constraint invariant on the mode
 - `𝑂` -- algorithm-specific options
 """
-function post(𝒫::BFFPSV18, 𝑆::AbstractSystem, invariant, 𝑂_input::Options)
+function post(𝒫::BFFPSV18, 𝑆::AbstractSystem, 𝑂_input::Options)
     𝑂 = TwoLayerOptions(merge(𝑂_input, 𝒫.options.specified), 𝒫.options.defaults)
 
     # convert matrix
@@ -255,7 +254,7 @@ function post(𝒫::BFFPSV18, 𝑆::AbstractSystem, invariant, 𝑂_input::Optio
     if 𝑂[:mode] == "reach"
         info("Reachable States Computation...")
         @timing begin
-            Rsets = reach(𝑆, invariant, 𝑂)
+            Rsets = reach(𝑆, 𝑂)
             info("- Total")
         end
 

src/ReachSets/ContinuousPost/BFFPSV18/reach.jl

@@ -7,14 +7,13 @@ import LazySets.Approximations: overapproximate
 import ProgressMeter: update!
 
 """
-    reach(S, invariant, options)
+    reach(problem, options)
 
 Interface to reachability algorithms for an LTI system.
 
 ### Input
 
-- `S`         -- LTI system, discrete or continuous
-- `invariant` -- invariant
+- `problem`   -- initial value problem
 - `options`   -- additional options
 
 ### Output
@@ -28,27 +27,26 @@ A dictionary with available algorithms is available via
 
 The numeric type of the system's coefficients and the set of initial states
 is inferred from the first parameter of the system (resp. lazy set), ie.
-`NUM = first(typeof(S.s).parameters)`.
+`NUM = first(typeof(problem.s).parameters)`.
 """
-function reach(S::Union{IVP{<:LDS{NUM}, <:LazySet{NUM}},
-                        IVP{<:CLCDS{NUM}, <:LazySet{NUM}}},
-               invariant::Union{LazySet, Nothing},
+function reach(problem::Union{IVP{<:CLDS{NUM}, <:LazySet{NUM}},
+                              IVP{<:CLCDS{NUM}, <:LazySet{NUM}}},
                options::TwoLayerOptions
               )::Vector{<:ReachSet} where {NUM <: Real}
 
     # list containing the arguments passed to any reachability function
     args = []
 
     # coefficients matrix
-    A = S.s.A
+    A = problem.s.A
     push!(args, A)
 
     # determine analysis mode (sparse/dense) for lazy_expm mode
     if A isa SparseMatrixExp
         push!(args, Val(options[:assume_sparse]))
     end
 
-    n = statedim(S)
+    n = statedim(problem)
     blocks = options[:blocks]
     partition = convert_partition(options[:partition])
     T = options[:T]
@@ -58,11 +56,11 @@ function reach(S::Union{IVP{<:LDS{NUM}, <:LazySet{NUM}},
     if length(partition) == 1 && length(partition[1]) == n &&
             options[:block_options_init] == LinearMap
         info("- Skipping decomposition of X0")
-        Xhat0 = LazySet{NUM}[S.x0]
+        Xhat0 = LazySet{NUM}[problem.x0]
     else
         info("- Decomposing X0")
         @timing begin
-            Xhat0 = array(decompose(S.x0, options[:partition],
+            Xhat0 = array(decompose(problem.x0, options[:partition],
                                     options[:block_options_init]))
         end
     end
@@ -90,8 +88,8 @@ function reach(S::Union{IVP{<:LDS{NUM}, <:LazySet{NUM}},
     push!(args, Xhat0)
 
     # inputs
-    if !options[:assume_homogeneous] && inputdim(S) > 0
-        U = inputset(S)
+    if !options[:assume_homogeneous] && inputdim(problem) > 0
+        U = inputset(problem)
     else
         U = nothing
     end
@@ -162,6 +160,7 @@ function reach(S::Union{IVP{<:LDS{NUM}, <:LazySet{NUM}},
     push!(args, options[:δ])
 
     # termination function
+    invariant = stateset(problem.s)
     termination = get_termination_function(N, invariant)
     push!(args, termination)
 
@@ -201,30 +200,28 @@ function reach(S::Union{IVP{<:LDS{NUM}, <:LazySet{NUM}},
     return res
 end
 
-function reach(system::IVP{<:AbstractContinuousSystem},
-               invariant::Union{LazySet, Nothing},
+function reach(problem::Union{IVP{<:CLCS{NUM}, <:LazySet{NUM}},
+                              IVP{<:CLCCS{NUM}, <:LazySet{NUM}}},
                options::TwoLayerOptions
-              )::Vector{<:ReachSet}
-    # ===================
-    # Time discretization
-    # ===================
+              )::Vector{<:ReachSet} where {NUM <: Real}
+
     info("Time discretization...")
-    Δ = @timing discretize(system, options[:δ], algorithm=options[:discretization],
-                                                exp_method=options[:exp_method],
-                                                sih_method=options[:sih_method])
+    Δ = @timing discretize(problem, options[:δ], algorithm=options[:discretization],
+                                                 exp_method=options[:exp_method],
+                                                 sih_method=options[:sih_method])
 
     Δ = matrix_conversion(Δ, options)
-    return reach(Δ, invariant, options)
+    return reach(Δ, options)
 end
 
-function get_termination_function(N::Nothing, invariant::Nothing)
+function get_termination_function(N::Nothing, invariant::Universe)
     termination_function = (k, set, t0) -> termination_unconditioned()
     warn("no termination condition specified; the reachability analysis will " *
          "not terminate")
     return termination_function
 end
 
-function get_termination_function(N::Int, invariant::Nothing)
+function get_termination_function(N::Int, invariant::Universe)
     return (k, set, t0) -> termination_N(N, k, t0)
 end
 

src/ReachSets/discretize.jl

@@ -1,8 +1,3 @@
-const LDS = LinearDiscreteSystem
-const CLCDS = ConstrainedLinearControlDiscreteSystem
-
-@inline Id(n) = Matrix(1.0I, n, n)
-
 """
     discretize(𝑆, δ; [algorithm], [exp_method], [sih_method], [set_operations])
 
@@ -416,7 +411,7 @@ function discretize_firstorder(𝑆::InitialValueProblem,
         α = κ * RX0
         □α = Ballp(p, zeros(n), α)
         Ω0 = ConvexHull(X0, ϕ * X0 ⊕ □α)
-        return IVP(LDS(ϕ), Ω0)
+        return IVP(CLDS(ϕ, stateset(𝑆.s)), Ω0)
 
     elseif isaffine(𝑆)
         Uset = inputset(𝑆)
@@ -435,7 +430,7 @@ function discretize_firstorder(𝑆::InitialValueProblem,
             # transformation of the inputs
             □β = Ballp(p, zeros(n), β)
             Ud = ConstantInput(δ*U ⊕ □β)
-            return IVP(CLCDS(ϕ, Id(n), nothing, Ud), Ω0)
+            return IVP(CLCDS(ϕ, I(n), stateset(𝑆.s), Ud), Ω0)
 
         elseif Uset isa VaryingInput
             Ud = Vector{LazySet}(undef, length(Uset))
@@ -457,7 +452,7 @@ function discretize_firstorder(𝑆::InitialValueProblem,
                 Ud[i] = δ*Ui ⊕ □β
             end
             Ud = VaryingInput(Ud)
-            return IVP(CLCDS(ϕ, Id(n), nothing, Ud), Ω0)
+            return IVP(CLCDS(ϕ, I(n), stateset(𝑆.s), Ud), Ω0)
         else
             throw(ArgumentError("input of type $(typeof(U)) is not allowed"))
         end
@@ -525,6 +520,7 @@ function  discretize_nobloating(𝑆::InitialValueProblem{<:AbstractContinuousSy
 
     # unwrap coefficient matrix and initial states
     A, X0 = 𝑆.s.A, 𝑆.x0
+    n = size(A, 1)
 
     # compute matrix ϕ = exp(Aδ)
     ϕ = exp_Aδ(A, δ, exp_method=exp_method)
@@ -534,15 +530,15 @@ function  discretize_nobloating(𝑆::InitialValueProblem{<:AbstractContinuousSy
 
     # early return for homogeneous systems
     if inputdim(𝑆) == 0
-        return IVP(LDS(ϕ), Ω0)
+        return IVP(CLDS(ϕ, stateset(𝑆.s)), Ω0)
     end
 
     # compute matrix to transform the inputs
     Phi1Adelta = Φ₁(A, δ, exp_method=exp_method)
     U = inputset(𝑆)
     Ud = map(ui -> Phi1Adelta * ui, U)
 
-    return IVP(CLCDS(ϕ, Id(size(A, 1)), nothing, Ud), Ω0)
+    return IVP(CLCDS(ϕ, I(n), stateset(𝑆.s), Ud), Ω0)
 end
 
 """
@@ -646,7 +642,7 @@ function discretize_interpolation(𝑆::InitialValueProblem{<:AbstractContinuous
     # early return for homogeneous systems
     if inputdim(𝑆) == 0
         Ω0 = _discretize_interpolation_homog(X0, ϕ, Einit, Val(set_operations))
-        return IVP(LDS(ϕ), Ω0)
+        return IVP(CLDS(ϕ, stateset(𝑆.s)), Ω0)
     end
 
     U = inputset(𝑆)
@@ -655,7 +651,7 @@ function discretize_interpolation(𝑆::InitialValueProblem{<:AbstractContinuous
     Eψ0 = sih(Phi2Aabs * sih(A * U0))
     Ω0, Ud = _discretize_interpolation_inhomog(δ, U0, U, X0, ϕ, Einit, Eψ0, A, sih, Phi2Aabs, Val(set_operations))
 
-    return IVP(CLCDS(ϕ, Id(size(A, 1)), nothing, Ud), Ω0)
+    return IVP(CLCDS(ϕ, I(size(A, 1)), stateset(𝑆.s), Ud), Ω0)
 end
 
 # version using lazy sets and operations

src/Reachability.jl

@@ -11,28 +11,19 @@ using Reexport, RecipesBase, Memento, MathematicalSystems, HybridSystems,
 import LazySets.use_precise_ρ
 import LazySets.LinearMap
 
- # common aliases for MathematicalSystems types
- const CLCCS = ConstrainedLinearControlContinuousSystem
- const CLCDS = ConstrainedLinearControlDiscreteSystem
- const LCS = LinearContinuousSystem
- const LDS = LinearDiscreteSystem
-
 include("logging.jl")
-include("Utils/Utils.jl")
 include("Options/dictionary.jl")
 include("Options/validation.jl")
 include("Options/default_options.jl")
+include("Utils/Utils.jl")
 include("Properties/Properties.jl")
 include("ReachSets/ReachSets.jl")
-include("Transformations/Transformations.jl")
 
 @reexport using Reachability.Utils,
                 Reachability.ReachSets,
-                Reachability.Properties,
-                Reachability.Transformations
+                Reachability.Properties
 
-export project,
-       Transformations
+export project
 
 include("solve.jl")
 include("plot_recipes.jl")

src/Utils/Utils.jl

@@ -8,7 +8,7 @@ using LazySets, MathematicalSystems, HybridSystems
 
 include("../compat.jl")
 
-import Reachability.@timing
+using Reachability: Options
 
 # Visualization
 export print_sparsity,
@@ -41,6 +41,9 @@ include("systems.jl")
 # normalization
 include("normalization.jl")
 
+# coordinate transformations
+include("transformations.jl")
+
 # abstract solution type
 include("AbstractSolution.jl")