diff --git a/src/Options/BFFPSV18_options.jl b/src/Options/BFFPSV18_options.jl index 2778d946..d4fa5eaa 100644 --- a/src/Options/BFFPSV18_options.jl +++ b/src/Options/BFFPSV18_options.jl @@ -14,7 +14,6 @@ Supported options: - `:logfile` -- name of a log file - `:mode` -- main analysis mode - `:property` -- a safety property -- `:δ` -- time step; alias: `:sampling_time` - `:N` -- number of time steps - `:T` -- time horizon; alias `:time_horizon` - `:vars` -- variables of interest @@ -118,8 +117,8 @@ 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) - # special options: δ, N, T - check_and_add_δ_N_T!(dict, dict_copy) + # special option: T + check_aliases!(dict, dict_copy, [:T, :time_horizon]) # special option: plot_vars check_and_add_plot_vars!(dict, dict_copy) @@ -158,9 +157,6 @@ function validate_solver_options_and_add_default_values!(options::Options)::Opti end elseif key == :property expected_type = Union{Property, Nothing} - elseif key == :δ - expected_type = Float64 - domain_constraints = (v::Float64 -> v > 0.) elseif key == :N expected_type = Int domain_constraints = (v::Int -> v > 0) diff --git a/src/Options/validation.jl b/src/Options/validation.jl index 58626e9a..72a3240a 100644 --- a/src/Options/validation.jl +++ b/src/Options/validation.jl @@ -4,90 +4,6 @@ Validation methods for dictionaries of options available_keywords = Set{Symbol}([]) -""" - check_and_add_δ_N_T!(dict::Dict{Symbol,Any}, dict_copy::Dict{Symbol,Any}) - -Handling of the special trio `:δ`, `:N`, `:T`. -Usually two of them should be defined and the third one is automatically inferred. -If three of them are defined, they must be consistent. -If only `:T` is defined, we use `:N = 100`. - -### Input - -- `dict` -- a dictionary of options -- `dict_copy` -- a copy of the dictionary of options for internal names - -Supported options: - -- `:δ` (time step) -- alias: `:sampling_time` -- `:N` (number of time steps) -- `:T` (time horizon) -- alias: `:time_horizon` -""" -function check_and_add_δ_N_T!(dict::Dict{Symbol,Any}, dict_copy::Dict{Symbol,Any}) - δ_aliases = [:δ, :sampling_time] - T_aliases = [:T, :time_horizon] - check_aliases!(dict, dict_copy, δ_aliases) - check_aliases!(dict, dict_copy, [:N]) - check_aliases!(dict, dict_copy, T_aliases) - - defined = 0 - if haskey(dict_copy, :δ) - value = dict_copy[:δ] - if !(value isa Float64 && value > 0.) - error("$value is not a valid value for option $δ_aliases.") - end - defined += 1 - end - if haskey(dict_copy, :N) - value = dict_copy[:N] - if !(value isa Int && value > 0) - error("$value is not a valid value for option :N.") - end - defined += 1 - end - if haskey(dict_copy, :T) - value = dict_copy[:T] - if !(value isa Float64 && value > 0.) - error("$value is not a valid value for option $T_aliases.") - end - defined += 1 - end - - if defined == 1 && haskey(dict_copy, :T) - N = 100 - dict[:N] = N - dict_copy[:N] = N - δ = dict_copy[:T] / dict_copy[:N] - dict[:δ] = δ - dict_copy[:δ] = δ - elseif defined == 2 - if !haskey(dict_copy, :δ) - δ = dict_copy[:T] / dict_copy[:N] - dict[:δ] = δ - dict_copy[:δ] = δ - end - if !haskey(dict_copy, :N) - N = (Int)(ceil(dict_copy[:T] / dict_copy[:δ])) - dict[:N] = N - dict_copy[:N] = N - end - if !haskey(dict_copy, :T) - T = dict_copy[:N] * dict_copy[:δ] - dict[:T] = T - dict_copy[:T] = T - end - elseif defined == 3 - N_computed = (Int)(ceil(dict_copy[:T] / dict_copy[:δ])) - if N_computed != dict_copy[:N] - error("Values for :δ ($(dict_copy[:δ])), :N ($(dict_copy[:N])), and :T ($(dict_copy[:T])) were defined, but they are inconsistent.") - end - else - error("Need two of the following options: :δ, :N, :T (or at least :T and using default values)") - end -end - """ check_and_add_plot_vars!(dict::Dict{Symbol,Any}, dict_copy::Dict{Symbol,Any}) diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl index 0ad9504d..1760b16e 100644 --- a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl +++ b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl @@ -11,6 +11,8 @@ function options_BFFPSV18() info="model for bloating/continuous time analysis"), OptionSpec(:algorithm, "explicit", domain=String, domain_check=( v -> v in ["explicit", "wrap"]), info="algorithm backend"), + OptionSpec(:δ, 1e-2, domain=Float64, aliases=[:sampling_time], + domain_check=(v -> v > 0.), info="time step"), ] end diff --git a/src/ReachSets/project_reach.jl b/src/ReachSets/project_reach.jl index b327c0ce..e5b01136 100644 --- a/src/ReachSets/project_reach.jl +++ b/src/ReachSets/project_reach.jl @@ -81,7 +81,6 @@ function project_reach( RsetsProj = Vector{ReachSet{set_type{numeric_type}, numeric_type}}(undef, N) end - δ = options[:δ] if got_time @inbounds for i in 1:N t0 = Rsets[i].t_start @@ -174,7 +173,6 @@ function project_2d_reach( RsetsProj = Vector{ReachSet{set_type{numeric_type}, numeric_type}}(undef, N) end - δ = options[:δ] if output_function @inbounds for i in 1:N t0 = Rsets[i].t_start diff --git a/test/Properties/unit_tune.jl b/test/Properties/unit_tune.jl index 0fd2d0a9..5f035d58 100644 --- a/test/Properties/unit_tune.jl +++ b/test/Properties/unit_tune.jl @@ -1,3 +1,5 @@ +using Reachability.ReachSets: BFFPSV18 + #===== Projectile model ===== We test the line plot!(x->x, x->-24*x+375, 0., 50., line=2., color="red", linestyle=:solid, legend=:none) =# @@ -8,9 +10,11 @@ S = ContinuousSystem(A, X0, U) time_horizon = 20.0 prec = 1e-4 initial_δ = 0.5 -algorithm(N, δ) = solve(S, :mode => "check", :partition=>[1:2, 3:4], - :vars => [1, 3], :plot_vars => [1, 3], :δ => δ, - :T => time_horizon, - :property=>LinearConstraintProperty([24., 0., 1, 0], 375.)).satisfied +algorithm(N, δ) = solve(S, + Options(:mode => "check", :partition=>[1:2, 3:4], + :vars => [1, 3], :plot_vars => [1, 3], + :T => time_horizon, + :property=>LinearConstraintProperty([24., 0., 1, 0], 375.)); + op=BFFPSV18(:δ => δ)).satisfied Reachability.tune_δ(algorithm, time_horizon, prec, initial_δ) diff --git a/test/Reachability/models/bouncing_ball.jl b/test/Reachability/models/bouncing_ball.jl index 523f591d..87119e69 100644 --- a/test/Reachability/models/bouncing_ball.jl +++ b/test/Reachability/models/bouncing_ball.jl @@ -43,7 +43,7 @@ function bouncing_ball() system = InitialValueProblem(ℋ, initial_condition) - options = Options(:mode=>"reach", :vars=>[1, 2], :T=>5.0, :δ=>0.1, + options = Options(:mode=>"reach", :vars=>[1, 2], :T=>5.0, :plot_vars=>[1, 2], :max_jumps=>1, :verbosity=>1) return (system, options) diff --git a/test/Reachability/models/thermostat.jl b/test/Reachability/models/thermostat.jl index 786e7772..86028c12 100644 --- a/test/Reachability/models/thermostat.jl +++ b/test/Reachability/models/thermostat.jl @@ -56,7 +56,7 @@ function thermostat() system = InitialValueProblem(ℋ, initial_condition) - options = Options(:mode=>"reach", :vars=>[1], :T=>5.0, :δ=>0.1, + options = Options(:mode=>"reach", :vars=>[1], :T=>5.0, :max_jumps=>1, :verbosity=>1) return (system, options) diff --git a/test/Reachability/solve_hybrid.jl b/test/Reachability/solve_hybrid.jl index 53bb4630..4e37edb2 100644 --- a/test/Reachability/solve_hybrid.jl +++ b/test/Reachability/solve_hybrid.jl @@ -11,17 +11,19 @@ for model in models # --- reachability algorithms --- + opC = BFFPSV18(:δ=>0.1) + # default algorithm sol = solve(system, options) # concrete discrete-post operator - sol = solve(system, options, BFFPSV18(), ConcreteDiscretePost()) + sol = solve(system, options, opC, ConcreteDiscretePost()) # lazy discrete-post operator - sol = solve(system, options, BFFPSV18(), LazyDiscretePost()) + sol = solve(system, options, opC, LazyDiscretePost()) # overapproximating discrete-post operator - sol = solve(system, options, BFFPSV18(), ApproximatingDiscretePost()) + sol = solve(system, options, opC, ApproximatingDiscretePost()) # --- model analysis ---