Add checking property for flowpipes with mixed dimensions

src/Properties/BadStatesProperty.jl

@@ -70,3 +70,8 @@ Let ``Y`` be the bad states represented by 𝑃.
 @inline function check(𝑃::BadStatesProperty, X::LazySet; witness::Bool=false)
     return isdisjoint(X, 𝑃.bad, witness)
 end
+
+@inline function project(𝑃::BadStatesProperty, vars::AbstractVector{Int})
+    proj = project(𝑃.bad, vars)
+    return BadStatesProperty(proj)
+end

src/Properties/Conjunction.jl

@@ -75,3 +75,7 @@ function check(𝑃::Conjunction, X::LazySet{N};
     end
     return witness ? (true, N[]) : true
 end
+
+@inline function project(𝑃::Conjunction, vars::AbstractVector{Int})
+    return Conjunction([project(conjunct, vars) for conjunct in 𝑃.conjuncts])
+end

src/Properties/Disjunction.jl

@@ -114,3 +114,7 @@ function _reorder!(𝑃::Disjunction, i::Int)
     𝑃.disjuncts[1] = first
     return nothing
 end
+
+@inline function project(𝑃::Disjunction, vars::AbstractVector{Int})
+    return Disjunction([project(disjunct, vars) for disjunct in 𝑃.disjuncts])
+end

src/Properties/Properties.jl

@@ -7,14 +7,16 @@ module Properties
 using LazySets
 
 import LazySets.dim
+import LazySets.Approximations: project
 
 # ==============================
 # Property struct and evaluation
 # ==============================
 include("Property.jl")
 export Property,
        dim,
-       check
+       check,
+       project
 
 include("Conjunction.jl")
 include("Disjunction.jl")

src/Properties/SafeStatesProperty.jl

@@ -70,3 +70,8 @@ Let ``Y`` be the safe states represented by 𝑃.
 @inline function check(𝑃::SafeStatesProperty, X::LazySet; witness::Bool=false)
     return ⊆(X, 𝑃.safe, witness)
 end
+
+@inline function project(𝑃::SafeStatesProperty, vars::AbstractVector{Int})
+    proj = project(𝑃.safe, vars)
+    return SafeStatesProperty(proj)
+end

src/ReachSets/ContinuousPost/BFFPS19/reach.jl

@@ -191,7 +191,11 @@ function reach_mixed(problem::Union{IVP{<:CLDS{NUM}, <:LazySet{NUM}},
         invariant = LazySets.Approximations.project(invariant, vars)
     end
     termination = get_termination_function_out(N, invariant)
-    push!(args, options[:guards_proj])
+    if length(options[:guards_proj]) > 0
+        push!(args, options[:guards_proj])
+    else
+        push!(args, [Universe{NUM}(length(vars))])
+    end
     push!(args, options[:block_options_iter])
     push!(args, vars)
     push!(args, termination)

src/ReachSets/ContinuousPost/BFFPS19/reach_blocks.jl

@@ -135,7 +135,7 @@ function reach_blocks!(ϕ::SparseMatrixCSC{NUM, Int},
 
         terminate, skip, reach_set_intersected = termination(k, X_store, t0)
         if reach_set_intersected isa EmptySet
-            store!(res, k, X_store_d, t0, t1, N)
+            store!(res, k, X_store, t0, t1, N)
             break
         end
         if !(isdisjoint(reach_set_intersected, UnionSetArray(guards_proj)))
@@ -244,7 +244,7 @@ function reach_blocks!(ϕ::AbstractMatrix{NUM},
         t1 += δ
         terminate, skip, reach_set_intersected = termination(k, X_store, t0)
         if reach_set_intersected isa EmptySet
-            store!(res, k, X_store_d, t0, t1, N)
+            store!(res, k, X_store, t0, t1, N)
             break
         end
         if !(isdisjoint(reach_set_intersected, UnionSetArray(guards_proj)))

src/Reachability.jl

@@ -11,6 +11,8 @@ using Reexport, RecipesBase, Memento, MathematicalSystems, HybridSystems,
 import LazySets: use_precise_ρ
 using LazySets: LinearMap, AffineMap, ResetMap
 
+import LazySets.Approximations: project
+
 include("logging.jl")
 include("Options/dictionary.jl")
 include("Options/validation.jl")
@@ -23,8 +25,6 @@ include("ReachSets/ReachSets.jl")
                 Reachability.ReachSets,
                 Reachability.Properties
 
-export project
-
 include("solve.jl")
 include("plot_recipes.jl")
 

src/solve.jl

@@ -181,9 +181,27 @@ function solve!(system::InitialValueProblem{<:HybridSystem,
                        get(property, loc_id, nothing) :
                        property
         if property_loc != nothing
-            for (i, reach_set) in enumerate(reach_tube.Xk)
-                if !check(property_loc, reach_set.X)
-                    return CheckSolution(false, i, options)
+            if opD isa DecomposedDiscretePost
+                temp_vars = opD.options[:temp_vars]
+                n_lowdim = length(temp_vars)
+                n = dim(X0.X)
+                property_loc_lowdim = project(property_loc, temp_vars)
+                for (i, reach_set) in enumerate(reach_tube.Xk)
+                    if (dim(reach_set.X) == n_lowdim && n_lowdim < n)
+                        if !check(property_loc_lowdim, reach_set.X)
+                            return CheckSolution(false, i, options)
+                        end
+                    else
+                        if !check(property_loc, reach_set.X)
+                            return CheckSolution(false, i, options)
+                        end
+                    end
+                end
+            else
+                for (i, reach_set) in enumerate(reach_tube.Xk)
+                    if !check(property_loc, reach_set.X)
+                        return CheckSolution(false, i, options)
+                    end
                 end
             end
         end

test/Reachability/solve_hybrid.jl

@@ -55,5 +55,16 @@ for model in models
         @test constrained_dimensions(HS) == Dict{Int,Vector{Int}}(1=>[1, 2])
     elseif model == thermostat
         @test constrained_dimensions(HS) == Dict{Int,Vector{Int}}(1=>[1], 2=>[1])
+
+        opC = BFFPS19(:δ=>0.1)
+
+        prop_poly = HPolyhedron([HalfSpace([1.], 17.5)])
+        property = BadStatesProperty(prop_poly)
+
+        options[:property]= property
+        options[:mode]= "check"
+
+        sol = solve(system, options, opC, DecomposedDiscretePost())
+        @test sol.satisfied == true
     end
 end