Merge pull request #560 from JuliaReach/mforets/559

#559 - Accept CA_S in normalization
JuliaReach · Mar 19, 2019 · e982af8 · e982af8
2 parents 3cc0b1a + 973bb48
commit e982af8
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 3 deletions.
diff --git a/src/Utils/normalization.jl b/src/Utils/normalization.jl
@@ -98,15 +98,28 @@ for CLC_S in (:CLCCS, :CLCDS)
     end
 end
 
+# x' = Ax + c, x ∈ X, u ∈ U in the continuous case
+# x+ = Ax + c, x ∈ X, u ∈ U in the discrete case
+for (CA_S, CLC_S) in ((:CACS, :CLCCS), (:CADS, :CLCDS))
+    @eval begin
+        function normalize(system::$CA_S{N, AN, VN, XT}) where {N, AN<:AbstractMatrix{N}, VN<:AbstractVector{N}, XT<:XNCF{N}}
+            n = statedim(system)
+            X = _wrap_invariant(system.X, n)
+            U = _wrap_inputs(system.b)
+            $CLC_S(system.A, I(n, N), X, U)
+        end
+    end
+end
+
 # x' = Ax + Bu + c, x ∈ X, u ∈ U in the continuous case
 # x+ = Ax + Bu + c, x ∈ X, u ∈ U in the discrete case
-for CAC_S in (:CACCS, :CACDS)
+for (CAC_S, CLC_S) in ((:CACCS, :CLCCS), (:CACDS, :CLCDS))
     @eval begin
         function normalize(system::$CAC_S{N, AN, BN, VN, XT, UT}) where {N, AN<:AbstractMatrix{N}, BN<:AbstractMatrix{N}, VN<:AbstractVector{N}, XT<:XNCF{N}, UT<:UNCF{N}}
             n = statedim(system)
             X = _wrap_invariant(system.X, n)
             U = _wrap_inputs(system.U, system.B, system.c)
-            $CAC_S(system.A, I(n, N), X, U)
+            $CLC_S(system.A, I(n, N), X, U)
         end
     end
 end
@@ -134,6 +147,8 @@ _wrap_inputs(U::LazySet, B::AbstractMatrix, c::AbstractVector) = ConstantInput(B
 _wrap_inputs(U::Vector{<:LazySet}, B::IdentityMultiple, c::AbstractVector) = isidentity(B) ? VaryingInput(map(u -> u ⊕ c, U)) : VaryingInput(map(u -> B*u ⊕ c, U))
 _wrap_inputs(U::Vector{<:LazySet}, B::AbstractMatrix, c::AbstractVector) = VaryingInput(map(u -> B*u ⊕ c, U))
 
+_wrap_inputs(c::AbstractVector) = ConstantInput(Singleton(c))
+
 """
     distribute_initial_set(system::InitialValueProblem{<:HybridSystem, <:LazySet)
 

diff --git a/src/Utils/systems.jl b/src/Utils/systems.jl
@@ -12,6 +12,8 @@ const CLCCS = ConstrainedLinearControlContinuousSystem
 const CLCDS = ConstrainedLinearControlDiscreteSystem
 const CACCS = ConstrainedAffineControlContinuousSystem
 const CACDS = ConstrainedAffineControlDiscreteSystem
+const CACS = ConstrainedAffineContinuousSystem
+const CADS = ConstrainedAffineDiscreteSystem
 
 export LCS, LDS, CLCS, CLDS, CLCCS, CLCDS, CACCS, CACDS, IVP
 

diff --git a/src/solve.jl b/src/solve.jl
@@ -16,7 +16,7 @@ discrete or continuous system.
 A continuous post operator with default options.
 """
 function default_operator(system::InitialValueProblem)
-    if islinear(system)
+    if isaffine(system)
         op = BFFPSV18()
     else
         error("no default reachability algorithm available for system of " *

diff --git a/test/Reachability/solve_continuous.jl b/test/Reachability/solve_continuous.jl
@@ -157,3 +157,16 @@ s = Reachability.solve(IVP(CLCCS(A, B, X, U), X0), Options(:T=>Inf))
 s = solve(IVP(LCS(A), X0), :T=>Inf, :mode=>"check", :property=>property)
 s = solve(IVP(CLCCS(A, B, X, U), X0),
           :T=>Inf, :mode=>"check", :property=>property)
+
+# =================================================================
+# Affine ODE with a nondeterministic input, x' = Ax + b, no inputs
+# =================================================================
+A = [ 0.0509836  0.168159  0.95246   0.33644
+      0.42377    0.67972   0.129232  0.126662
+      0.518654   0.981313  0.489854  0.588326
+      0.38318    0.616014  0.518412  0.778765]
+b =  [1.0, -1, 0, 1.]
+X = HalfSpace([-1.0, 0.0, 0.0, 0.0], 0.0)
+X0 = BallInf(zeros(4), 0.5)
+p = IVP(ConstrainedAffineContinuousSystem(A, b, X), X0)
+sol = solve(p, :T=>0.1)