Skip to content

Commit

Permalink
move options for approximation
Browse files Browse the repository at this point in the history
  • Loading branch information
@schillic
schillic committed Feb 18, 2019
1 parent f858236 commit 6e439fa
Show file tree
Hide file tree
Showing 3 changed files with 116 additions and 142 deletions.
139 changes: 7 additions & 132 deletions src/Options/BFFPSV18_options.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)

Expand All @@ -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"])
Expand Down Expand Up @@ -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
97 changes: 97 additions & 0 deletions src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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)
Expand All @@ -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

Expand Down
22 changes: 12 additions & 10 deletions test/Reachability/solve_continuous.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]))
Expand Down Expand Up @@ -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),
Expand All @@ -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]])))
Expand All @@ -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
Expand Down

0 comments on commit 6e439fa

Please sign in to comment.