From 8a6b9396c11d70f785b007d0021d3bc53808bbb0 Mon Sep 17 00:00:00 2001 From: Kostiantyn Potomkin Date: Fri, 16 Aug 2019 19:50:41 +1000 Subject: [PATCH] add checking aproperty for DecomposedDiscretePost --- src/Properties/BadStatesProperty.jl | 5 ++++ src/Properties/Conjunction.jl | 4 ++++ src/Properties/Disjunction.jl | 4 ++++ src/Properties/Properties.jl | 4 +++- src/Properties/SafeStatesProperty.jl | 5 ++++ src/ReachSets/ContinuousPost/BFFPS19/reach.jl | 6 ++++- .../ContinuousPost/BFFPS19/reach_blocks.jl | 4 ++-- src/Reachability.jl | 4 ++-- src/solve.jl | 24 ++++++++++++++++--- test/Reachability/solve_hybrid.jl | 11 +++++++++ 10 files changed, 62 insertions(+), 9 deletions(-) diff --git a/src/Properties/BadStatesProperty.jl b/src/Properties/BadStatesProperty.jl index 9dd5be10..f451b3f4 100644 --- a/src/Properties/BadStatesProperty.jl +++ b/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 diff --git a/src/Properties/Conjunction.jl b/src/Properties/Conjunction.jl index 0d6e63b6..13b5c038 100644 --- a/src/Properties/Conjunction.jl +++ b/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 diff --git a/src/Properties/Disjunction.jl b/src/Properties/Disjunction.jl index 84d0cc9e..a4a40dd7 100644 --- a/src/Properties/Disjunction.jl +++ b/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 diff --git a/src/Properties/Properties.jl b/src/Properties/Properties.jl index 18dac92f..5c47b501 100644 --- a/src/Properties/Properties.jl +++ b/src/Properties/Properties.jl @@ -7,6 +7,7 @@ module Properties using LazySets import LazySets.dim +import LazySets.Approximations: project # ============================== # Property struct and evaluation @@ -14,7 +15,8 @@ import LazySets.dim include("Property.jl") export Property, dim, - check + check, + project include("Conjunction.jl") include("Disjunction.jl") diff --git a/src/Properties/SafeStatesProperty.jl b/src/Properties/SafeStatesProperty.jl index 87e60b0e..d8c6d2a5 100644 --- a/src/Properties/SafeStatesProperty.jl +++ b/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 diff --git a/src/ReachSets/ContinuousPost/BFFPS19/reach.jl b/src/ReachSets/ContinuousPost/BFFPS19/reach.jl index dad23d5e..da95a3ab 100644 --- a/src/ReachSets/ContinuousPost/BFFPS19/reach.jl +++ b/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) diff --git a/src/ReachSets/ContinuousPost/BFFPS19/reach_blocks.jl b/src/ReachSets/ContinuousPost/BFFPS19/reach_blocks.jl index d5649251..640c55b5 100644 --- a/src/ReachSets/ContinuousPost/BFFPS19/reach_blocks.jl +++ b/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))) diff --git a/src/Reachability.jl b/src/Reachability.jl index e7186af3..ecc634fc 100644 --- a/src/Reachability.jl +++ b/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") diff --git a/src/solve.jl b/src/solve.jl index 1b005e4e..07124a21 100644 --- a/src/solve.jl +++ b/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 diff --git a/test/Reachability/solve_hybrid.jl b/test/Reachability/solve_hybrid.jl index b17de9a4..b4210bc7 100644 --- a/test/Reachability/solve_hybrid.jl +++ b/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