Merge pull request #503 from JuliaReach/mforets/revise_discretize

Revise discretize
JuliaReach · Mar 6, 2019 · 2c63c5a · 2c63c5a
2 parents cfbbbfd + 4bd0920
commit 2c63c5a
Show file tree

Hide file tree

Showing 17 changed files with 693 additions and 382 deletions.
diff --git a/docs/src/lib/discretize.md b/docs/src/lib/discretize.md
@@ -11,17 +11,7 @@ CurrentModule = Reachability.ReachSets
 
 ```@docs
 discretize
-```
-
-## Dense-time reachability
-
-```@docs
-discr_bloat_firstorder
-discr_bloat_interpolation
-```
-
-## Discrete-time reachability
-
-```@docs
-discr_no_bloat
+discretize_interpolation
+discretize_firstorder
+discretize_nobloating
 ```
diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl
@@ -24,8 +24,7 @@ end
 function options_BFFPSV18()
     return OptionSpec[
         # general options
-        OptionSpec(:approx_model, "forward", domain=String, domain_check=(
-            v  ->  v in ["forward", "backward", "firstorder", "nobloating"]),
+        OptionSpec(:discretization, "forward", domain=String,
             info="model for bloating/continuous time analysis"),
         OptionSpec(:algorithm, "explicit", domain=String, domain_check=(
             v  ->  v in ["explicit", "wrap"]), info="algorithm backend"),
@@ -41,16 +40,10 @@ function options_BFFPSV18()
                  "containing its indices"),
 
         # discretization options
-        OptionSpec(:lazy_sih, false, domain=Bool,
-            info="use a lazy symmetric interval hull in discretization?"),
-        OptionSpec(:lazy_expm, false, domain=Bool,
-            info="use a lazy matrix exponential all the time?"),
-        OptionSpec(:lazy_expm_discretize, false, domain=Bool,
-            info="use a lazy matrix exponential in discretization?"),
-        OptionSpec(:pade_expm, false, domain=Bool,
-            info="use the Padé approximant method (instead of Julia's " *
-                 " built-in 'exp') to compute the lazy matrix exponential " *
-                 "in discretization?"),
+        OptionSpec(:sih_method, "concrete", domain=String,
+            info="method to compute the symmetric interval hull in discretization"),
+        OptionSpec(:exp_method, "base", domain=String,
+            info="method to compute the matrix exponential"),
         OptionSpec(:assume_sparse, false, domain=Bool,
             info="use an analysis for sparse discretized matrices?"),
 
@@ -208,12 +201,6 @@ function normalization_BFFPSV18!(𝑂::TwoLayerOptions)
 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]
@@ -337,7 +324,6 @@ Calculate the reachable states of the given initial value problem using `BFFPSV1
 - `𝑂` -- algorithm-specific options
 """
 function post(𝒫::BFFPSV18, 𝑆::AbstractSystem, invariant, 𝑂::Options)
-    # TODO temporary hack for refactoring
     𝑂 = TwoLayerOptions(merge(𝑂, 𝒫.options.specified), 𝒫.options.defaults)
 
     # convert matrix

diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl b/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl
@@ -182,16 +182,9 @@ function check_property(S::IVP{<:AbstractContinuousSystem},
     # Time discretization
     # ===================
     info("Time discretization...")
-    Δ = @timing begin
-        discretize(
-            S,
-            options[:δ],
-            approx_model=options[:approx_model],
-            pade_expm=options[:pade_expm],
-            lazy_expm=options[:lazy_expm_discretize],
-            lazy_sih=options[:lazy_sih]
-        )
-    end
-    Δ = matrix_conversion_lazy_explicit(Δ, options)
+    Δ = @timing discretize(S, options[:δ], algorithm=options[:discretization],
+                                           exp_method=options[:exp_method],
+                                           sih_method=options[:sih_method])
+    Δ = matrix_conversion(Δ, options)
     return check_property(Δ, property, options)
 end
diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/reach.jl b/src/ReachSets/ContinuousPost/BFFPSV18/reach.jl
@@ -227,17 +227,11 @@ function reach(system::IVP{<:AbstractContinuousSystem},
     # Time discretization
     # ===================
     info("Time discretization...")
-    Δ = @timing begin
-        discretize(
-            system,
-            options[:δ],
-            approx_model=options[:approx_model],
-            pade_expm=options[:pade_expm],
-            lazy_expm=options[:lazy_expm_discretize],
-            lazy_sih=options[:lazy_sih]
-        )
-    end
-    Δ = matrix_conversion_lazy_explicit(Δ, options)
+    Δ = @timing discretize(system, options[:δ], algorithm=options[:discretization],
+                                                exp_method=options[:exp_method],
+                                                sih_method=options[:sih_method])
+
+    Δ = matrix_conversion(Δ, options)
     return reach(Δ, invariant, options)
 end