Merge pull request #621 from JuliaReach/schillic/620

#620 - overapproximate in LazyDiscretePost for singular map

Author: schillic

src/ReachSets/DiscretePost/LazyDiscretePost.jl

@@ -27,7 +27,7 @@ struct LazyDiscretePost <: DiscretePost
         check_aliases_and_add_default_value!(𝑂.dict, 𝑂copy.dict, [:overapproximation], Hyperrectangle)
         check_aliases_and_add_default_value!(𝑂.dict, 𝑂copy.dict, [:lazy_R⋂I], false)
         check_aliases_and_add_default_value!(𝑂.dict, 𝑂copy.dict, [:lazy_R⋂G], true)
-        check_aliases_and_add_default_value!(𝑂.dict, 𝑂copy.dict, [:lazy_A⌜R⋂G⌟], true)
+        check_aliases_and_add_default_value!(𝑂.dict, 𝑂copy.dict, [:lazy_A⌜R⋂G⌟], "invertible")
         check_aliases_and_add_default_value!(𝑂.dict, 𝑂copy.dict, [:lazy_A⌜R⋂G⌟⋂I], true)
         check_aliases_and_add_default_value!(𝑂.dict, 𝑂copy.dict, [:combine_invariant_guard], 𝑂copy[:lazy_R⋂I])
 
@@ -158,7 +158,9 @@ function post(𝒫::LazyDiscretePost,
 
             # apply assignment
             A⌜R⋂G⌟ = apply_assignment(𝒫, constrained_map, R⋂G)
-            if !𝒫.options[:lazy_A⌜R⋂G⌟]
+            if 𝒫.options[:lazy_A⌜R⋂G⌟] == "always" ||
+                    (𝒫.options[:lazy_A⌜R⋂G⌟] == "invertible" &&
+                     !isinvertible(constrained_map))
                 A⌜R⋂G⌟ = overapproximate(A⌜R⋂G⌟, oa)
             end
 

src/Utils/Utils.jl

@@ -37,6 +37,9 @@ export template_direction_symbols,
 export normalize,
        distribute_initial_set
 
+# others
+export isinvertible
+
 # Extension of MathematicalSystems for use inside Reachability.jl
 include("systems.jl")
 
@@ -378,4 +381,34 @@ function matrix_conversion(Δ, options; A_passed=nothing)
     return Δ
 end
 
+"""
+    isinvertible(map::AbstractMap)
+
+Check if the matrix of an affine map is invertible.
+
+### Input
+
+- `map` -- an affine map
+
+### Output
+
+`true` if the matrix is invertible.
+Because we use a sufficient criterion, there can be false positives.
+"""
+function isinvertible(map::AbstractMap)
+    throw(ArgumentError("isinvertible(::$(typeof(map))) is not implemented"))
+end
+function isinvertible(map::ConstrainedIdentityMap)
+    return true
+end
+function isinvertible(map::ConstrainedLinearMap)
+    return LazySets.isinvertible(map.A)
+end
+function isinvertible(map::ConstrainedAffineMap)
+    return LazySets.isinvertible(map.A)
+end
+function isinvertible(map::ConstrainedResetMap)
+    return false
+end
+
 end # module