move option :δ, remove option :N

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)

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})

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
 

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

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_δ)

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)

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)

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 ---