From 6e439faf8c03670d8d824731d44f25faf743096a Mon Sep 17 00:00:00 2001 From: schillic Date: Mon, 18 Feb 2019 09:31:13 +0100 Subject: [PATCH] move options for approximation --- src/Options/BFFPSV18_options.jl | 139 +----------------- .../ContinuousPost/BFFPSV18/BFFPSV18.jl | 97 ++++++++++++ test/Reachability/solve_continuous.jl | 22 +-- 3 files changed, 116 insertions(+), 142 deletions(-) diff --git a/src/Options/BFFPSV18_options.jl b/src/Options/BFFPSV18_options.jl index eb2b7dce..35a84f64 100644 --- a/src/Options/BFFPSV18_options.jl +++ b/src/Options/BFFPSV18_options.jl @@ -15,26 +15,10 @@ Supported options: - `:mode` -- main analysis mode - `:property` -- a safety property - `:T` -- time horizon; alias `:time_horizon` -- `:ε` -- short hand to set `:ε_init` and `:ε_iter` -- `:set_type` -- short hand to set `:set_type_init` and `:set_type_iter` -- `:ε_init` -- error bound for the approximation of the initial states - (during decomposition) -- `:set_type_init` -- set type for the approximation of the initial states - (during decomposition) -- `:ε_iter` -- error bound for the approximation of the states ``X_k``, - ``k>0`` -- `:set_type_iter` -- set type for the approximation of the states ``X_k``, - ``k>0`` - `:ε_proj` -- error bound for the approximation of the states during projection - `:set_type_proj` -- set type for the approximation of the states during projection -- `:template_directions` -- short hand to set `template_directions_init` - and `template_directions_iter` -- `:template_directions_init` -- directions to use for the approximation of the - initial states (during decomposition) -- `:template_directions_iter` -- directions to use for the approximation of the - states ``X_k``, ``k>0``, for each block - `:coordinate_transformation` -- coordinate transformation method - `:projection_matrix` -- projection matrix - `:project_reachset` -- switch for applying projection @@ -80,16 +64,12 @@ function validate_solver_options_and_add_default_values!(options::Options)::Opti check_aliases_and_add_default_value!(dict, dict_copy, [:n], nothing) check_aliases_and_add_default_value!(dict, dict_copy, [:transformation_matrix], nothing) check_aliases_and_add_default_value!(dict, dict_copy, [:plot_vars, :output_variables], [0, 1]) + check_aliases_and_add_default_value!(dict, dict_copy, [:ε_proj], Inf) + check_aliases_and_add_default_value!(dict, dict_copy, [:set_type_proj], Hyperrectangle) # special option: T check_aliases!(dict, dict_copy, [:T, :time_horizon]) - # special options: ε, ε_init, ε_iter, ε_proj, - # set_type, set_type_init, set_type_iter, set_type_proj, - # template_directions, template_directions_init, - # template_directions_iter - check_and_add_approximation!(dict, dict_copy) - # validate that all input keywords are recognized check_valid_option_keywords(dict) @@ -115,42 +95,12 @@ function validate_solver_options_and_add_default_values!(options::Options)::Opti elseif key == :T expected_type = Float64 domain_constraints = (v::Float64 -> v > 0.) - elseif key == :ε - expected_type = Float64 - domain_constraints = (v -> v > 0.) - elseif key == :ε_init - expected_type = Float64 - domain_constraints = (v -> v > 0.) - elseif key == :ε_iter - expected_type = Float64 - domain_constraints = (v -> v > 0.) elseif key == :ε_proj expected_type = Float64 domain_constraints = (v -> v > 0.) - elseif key == :set_type - expected_type = Union{Type{HPolygon}, Type{Hyperrectangle}, - Type{LazySets.Interval}} - elseif key == :set_type_init - expected_type = Union{Type{HPolygon}, Type{Hyperrectangle}, - Type{LazySets.Interval}} - elseif key == :set_type_iter - expected_type = Union{Type{HPolygon}, Type{Hyperrectangle}, - Type{LazySets.Interval}} elseif key == :set_type_proj expected_type = Union{Type{HPolygon}, Type{Hyperrectangle}, Type{LazySets.Interval}} - elseif key == :template_directions - expected_type = Symbol - domain_constraints = (v::Symbol -> v in [:box, :oct, :boxdiag, - :nothing]) - elseif key == :template_directions_init - expected_type = Symbol - domain_constraints = (v::Symbol -> v in [:box, :oct, :boxdiag, - :nothing]) - elseif key == :template_directions_iter - expected_type = Symbol - domain_constraints = (v::Symbol -> v in [:box, :oct, :boxdiag, - :nothing]) elseif key == :coordinate_transformation expected_type = String domain_constraints = (v::String -> v in ["", "schur"]) @@ -188,86 +138,11 @@ function validate_solver_options_and_add_default_values!(options::Options)::Opti error("$value is not a valid value for option :$key.") end end - - return options_copy -end - -""" - check_and_add_approximation!(dict::Dict{Symbol,Any}, - dict_copy::Dict{Symbol,Any}) - -Handling of the special options `:ε` and `:set_type` resp. the subcases -`:ε_init`, `:ε_iter`, `:ε_proj`, `:set_type_init`, `:set_type_iter`, -`:set_type_proj`, `:template_directions`, `:template_directions_init`, and -`:template_directions_iter`. - -### Input - -- `dict` -- dictionary of options -- `dict_copy` -- copy of the dictionary of options for internal names - -### Notes: - -`:ε` and `:set_type`, if defined, are used as fallbacks (if the more specific -options are undefined). -If both `:ε_init` and `:set_type_init` are defined, they must be consistent. -""" -function check_and_add_approximation!(dict::Dict{Symbol,Any}, - dict_copy::Dict{Symbol,Any}) - # fallback options - check_aliases!(dict, dict_copy, [:ε]) - check_aliases!(dict, dict_copy, [:set_type]) - check_aliases!(dict, dict_copy, [:template_directions]) - ε = haskey(dict, :ε) ? dict[:ε] : Inf - - # fallback set type - if haskey(dict, :set_type) - # use the provided set type - set_type = dict[:set_type] - elseif ε < Inf - # use polygons - set_type = HPolygon - else - # use hyperrectangles - set_type = Hyperrectangle + # ε-close approximation + if dict_copy[:ε_proj] < Inf && dict_copy[:set_type_proj] != HPolygon + throw(DomainError("ε-close approximation is only supported with the " * + "set type 'HPolygon'")) end - ε_init = (haskey(dict, :set_type_init) && dict[:set_type_init] == HPolygon) || - (!haskey(dict, :set_type_init) && set_type == HPolygon) ? ε : Inf - check_aliases_and_add_default_value!(dict, dict_copy, [:ε_init], ε_init) - - set_type_init = dict_copy[:ε_init] < Inf ? HPolygon : set_type - check_aliases_and_add_default_value!(dict, dict_copy, [:set_type_init], set_type_init) - - template_directions_init = haskey(dict, :template_directions_init) ? - dict[:template_directions_init] : haskey(dict, :template_directions) ? - dict[:template_directions] : :nothing - check_aliases_and_add_default_value!(dict, dict_copy, - [:template_directions_init], template_directions_init) - - ε_iter = (haskey(dict, :set_type_iter) && dict[:set_type_iter] == HPolygon) || - (!haskey(dict, :set_type_iter) && set_type == HPolygon) ? ε : Inf - check_aliases_and_add_default_value!(dict, dict_copy, [:ε_iter], ε_iter) - - set_type_iter = dict_copy[:ε_iter] < Inf ? HPolygon : set_type - check_aliases_and_add_default_value!(dict, dict_copy, [:set_type_iter], set_type_iter) - - template_directions_iter = haskey(dict, :template_directions_iter) ? - dict[:template_directions_iter] : haskey(dict, :template_directions) ? - dict[:template_directions] : :nothing - check_aliases_and_add_default_value!(dict, dict_copy, - [:template_directions_iter], template_directions_iter) - - ε_proj = (haskey(dict, :set_type_proj) && dict[:set_type_proj] == HPolygon) || - (!haskey(dict, :set_type_proj) && set_type == HPolygon) ? ε : - min(dict_copy[:ε_init], dict_copy[:ε_iter], ε) - check_aliases_and_add_default_value!(dict, dict_copy, [:ε_proj], ε_proj) - - set_type_proj = dict_copy[:ε_proj] < Inf ? HPolygon : Hyperrectangle - check_aliases_and_add_default_value!(dict, dict_copy, [:set_type_proj], set_type_proj) - - @assert (dict_copy[:ε_init] == Inf || dict_copy[:set_type_init] == HPolygon) && - (dict_copy[:ε_iter] == Inf || dict_copy[:set_type_iter] == HPolygon) && - (dict_copy[:ε_proj] == Inf || dict_copy[:set_type_proj] == HPolygon) ( - "ε-close approximation is only supported with the HPolygon set type") + return options_copy end diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl index 93f18156..c81c0ff3 100644 --- a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl +++ b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl @@ -78,6 +78,37 @@ function options_BFFPSV18() Dict{Type{<:LazySet}, AbstractVector{<:AbstractVector{Int}}}}, info="set type for the approximation of the states ``X_k``, " * "``k>0``, for each block"), + OptionSpec(:ε, Inf, domain=Float64, domain_check=(v -> v > 0.), + info="short hand to set `:ε_init` and `:ε_iter`"), + OptionSpec(:ε_init, Inf, domain=Float64, domain_check=(v -> v > 0.), + info="error bound for the approximation of the initial states" * + "(during decomposition)"), + OptionSpec(:ε_iter, Inf, domain=Float64, domain_check=(v -> v > 0.), + info="error bound for the approximation of the states ``X_k``, " * + "``k>0``"), + OptionSpec(:set_type, Hyperrectangle, domain=Union{Type{HPolygon}, + Type{Hyperrectangle}, Type{LazySets.Interval}}, + info="short hand to set `:set_type_init` and `:set_type_iter`"), + OptionSpec(:set_type_init, Hyperrectangle, domain=Union{Type{HPolygon}, + Type{Hyperrectangle}, Type{LazySets.Interval}}, + info="set type for the approximation of the initial states" * + "(during decomposition)"), + OptionSpec(:set_type_iter, Hyperrectangle, domain=Union{Type{HPolygon}, + Type{Hyperrectangle}, Type{LazySets.Interval}}, + info="set type for the approximation of the states ``X_k``, " * + "``k>0``"), + OptionSpec(:template_directions, :nothing, domain=Symbol, + domain_check=(v::Symbol -> v in [:box, :oct, :boxdiag, :nothing]), + info="short hand to set `template_directions_init` and " * + "`template_directions_iter`"), + OptionSpec(:template_directions_init, :nothing, domain=Symbol, + domain_check=(v::Symbol -> v in [:box, :oct, :boxdiag, :nothing]), + info="directions to use for the approximation of the initial " * + "states (during decomposition)"), + OptionSpec(:template_directions_iter, :nothing, domain=Symbol, + domain_check=(v::Symbol -> v in [:box, :oct, :boxdiag, :nothing]), + info="directions to use for the approximation of the states " * + "``X_k``, ``k>0``, for each block"), # convenience options OptionSpec(:assume_homogeneous, false, domain=Bool, @@ -116,15 +147,74 @@ function normalization_BFFPSV18!(𝑂::TwoLayerOptions) 𝑂.specified[:block_types_iter] = block_types end + # :ε, :set_type, and :template_directions options + ε = 𝑂[:ε] + if haskey_specified(𝑂, :set_type) + # use the provided set type + set_type = 𝑂[:set_type] + elseif ε < Inf + # use polygons + set_type = HPolygon + 𝑂[:set_type] = HPolygon + else + # use hyperrectangles + set_type = 𝑂[:set_type] + end + # + if !haskey_specified(𝑂, :ε_init) + 𝑂.specified[:ε_init] = + (haskey_specified(𝑂, :set_type_init) && 𝑂[:set_type_init] == HPolygon) || + (!haskey_specified(𝑂, :set_type_init) && set_type == HPolygon) ? + ε : + Inf + end + # + if !haskey_specified(𝑂, :set_type_init) + 𝑂.specified[:set_type_init] = 𝑂[:ε_init] < Inf ? HPolygon : set_type + end + # + if !haskey_specified(𝑂, :template_directions_init) + 𝑂.specified[:template_directions_init] = + haskey_specified(𝑂, :template_directions_init) ? + 𝑂[:template_directions_init] : + haskey_specified(𝑂, :template_directions) ? + 𝑂[:template_directions] : + :nothing + end + # + if !haskey_specified(𝑂, :ε_iter) + 𝑂.specified[:ε_iter] = + (haskey_specified(𝑂, :set_type_iter) && 𝑂[:set_type_iter] == HPolygon) || + (!haskey_specified(𝑂, :set_type_iter) && set_type == HPolygon) ? + ε : + Inf + end + # + if !haskey_specified(𝑂, :set_type_iter) + 𝑂.specified[:set_type_iter] = 𝑂[:ε_iter] < Inf ? HPolygon : set_type + end + # + if !haskey_specified(𝑂, :template_directions_iter) + 𝑂.specified[:template_directions_iter] = + haskey_specified(𝑂, :template_directions_iter) ? + 𝑂[:template_directions_iter] : + haskey_specified(𝑂, :template_directions) ? + 𝑂[:template_directions] : + :nothing + end + # + nothing end function validation_BFFPSV18(𝑂) + # lazy_expm_discretize & lazy_expm if !𝑂[:lazy_expm_discretize] && 𝑂[:lazy_expm] throw(DomainError(𝑂[:lazy_expm_discretize], "cannot use option " * "':lazy_expm' with deactivated option ':lazy_expm_discretize'")) end + # block_types if haskey_specified(𝑂, :block_types) for (key, value) in 𝑂[:block_types] if !(key <: LazySet) @@ -138,6 +228,13 @@ function validation_BFFPSV18(𝑂) end end + # ε-close approximation + if (𝑂[:ε_init] < Inf && 𝑂[:set_type_init] != HPolygon) || + (𝑂[:ε_iter] < Inf && 𝑂[:set_type_iter] != HPolygon) + throw(DomainError("ε-close approximation is only supported with the " * + "set type 'HPolygon'")) + end + nothing end diff --git a/test/Reachability/solve_continuous.jl b/test/Reachability/solve_continuous.jl index ff5620f4..54a60ca2 100644 --- a/test/Reachability/solve_continuous.jl +++ b/test/Reachability/solve_continuous.jl @@ -22,8 +22,7 @@ s = solve(ContinuousSystem(A, X0), Options(:T=>0.1), op=BFFPSV18(:vars=>[1,3], :partition=>[1:2, 3:4])) -# the default partition is used. uses Interval for set_type_init and set_type_iter -# but Hyperrectangle for set_type_proj +# the default partition is used. s = solve(ContinuousSystem(A, X0), Options(:T=>0.1), op=BFFPSV18(:vars=>[1,3])) @@ -65,8 +64,9 @@ s = solve(ContinuousSystem(A, X0), # template directions (eg. :box, :oct, :octbox) s = solve(ContinuousSystem(A, X0), - Options(:T=>0.1, :template_directions => :oct, :ε_proj=>1e-5), - op=BFFPSV18(:vars=>[1,3], :partition=>[1:4])) + Options(:T=>0.1, :ε_proj=>1e-5, :set_type_proj=>HPolygon), + op=BFFPSV18(:vars=>[1,3], :partition=>[1:4], + :template_directions => :oct)) s = solve(ContinuousSystem(A, X0), Options(:T=>0.1), @@ -86,18 +86,19 @@ s = solve(ContinuousSystem(sparse(A), X0), op=BFFPSV18(:vars=>[1,3], :partition=>[1:2, 3:4], :lazy_expm=>true, :lazy_expm_discretize=>true, :assume_sparse=>true)) +# uses Interval for set_type_init and set_type_iter but Hyperrectangle for +# set_type_proj s = solve(ContinuousSystem(sparse(A), X0), - Options(:T=>0.1, :set_type=>Interval), + Options(:T=>0.1), op=BFFPSV18(:vars=>[1,3], :partition=>[[i] for i in 1:4], - :lazy_expm=>true, :lazy_expm_discretize=>true)) + :lazy_expm=>true, :lazy_expm_discretize=>true, + :set_type=>Interval)) # =============================== # System with an odd dimension # =============================== A = randn(5, 5); X0 = BallInf(ones(5), 0.1) -system = ContinuousSystem(A, X0) -options = Options(:T=>0.1) -s = solve(system, options, +s = solve(ContinuousSystem(A, X0), Options(:T=>0.1), op=BFFPSV18(:vars=>[1,3], :partition=>[1:2, 3:4, [5]], :block_types=> Dict{Type{<:LazySet}, AbstractVector{<:AbstractVector{Int}}}( HPolygon=>[1:2, 3:4], Interval=>[[5]]))) @@ -108,7 +109,8 @@ s = solve(system, options, A = [1 2 1.; 0 0. 1; -2 1 4] X0 = BallInf(ones(3), 0.1) system = ContinuousSystem(A, X0) -s = solve(system, Options(:T=>0.1), op=BFFPSV18(:vars=>1:3, :partition=>[1:2, 3:3])) +s = solve(system, Options(:T=>0.1), + op=BFFPSV18(:vars=>1:3, :partition=>[1:2, 3:3])) # ======================================================= # Affine ODE with a nondeterministic input, x' = Ax + Bu