final changes before review of reach_blocks! and DecomposedDiscretePost

src/ReachSets/ContinuousPost/BFFPS19/BFFPS19.jl

@@ -51,8 +51,6 @@ function options_BFFPS19()
         # convenience options
         OptionSpec(:assume_homogeneous, false, domain=Bool,
             info="ignore dynamic inputs during the analysis?"),
-        OptionSpec(:eager_checking, true, domain=Bool,
-            info="terminate as soon as property violation was detected?"),
     ]
 end
 
@@ -166,7 +164,6 @@ BFFPS19(𝑂::Pair{Symbol,<:Any}...) = BFFPS19(Options(Dict{Symbol,Any}(𝑂)))
 # default options
 BFFPS19() = BFFPS19(Options())
 
-include("reach_helper.jl")
 include("reach.jl")
 include("reach_blocks.jl")
 

src/ReachSets/ContinuousPost/BFFPS19/reach.jl

@@ -6,6 +6,40 @@ using LazySets: CacheMinkowskiSum,
 import LazySets.Approximations: overapproximate
 import ProgressMeter: update!
 
+"""
+combine_cpas(cpa1::CartesianProductArray{N, S}, cpa2::CartesianProductArray{N, S},
+                       blocks1::Vector{Int}, blocks2::Vector{Int}) where {N, S<:LazySet{N}}
+
+Compose high-dimensional cartesian product array from 2 low-dimensional CPA's
+
+### Input
+
+- `cpa1`   -- Cartesian Product Array
+- `cpa2`   -- Cartesian Product Array
+- `blocks1`   -- Block structure of cpa1 in sense of high-dimensional set
+- `blocks2`   -- Block structure of cpa2 in sense of high-dimensional set
+
+### Output
+
+A sequence of [`ReachSet`](@ref)s.
+
+### Notes
+
+A dictionary with available algorithms is available via
+`Reachability.available_algorithms`.
+
+The numeric type of the system's coefficients and the set of initial states
+is inferred from the first parameter of the system (resp. lazy set), ie.
+`NUM = first(typeof(problem.s).parameters)`.
+"""
+function combine_cpas(cpa1::CartesianProductArray{N, S}, cpa2::CartesianProductArray{N, S},
+                       blocks1::Vector{Int}, blocks2::Vector{Int}) where {N, S<:LazySet{N}}
+    result = Vector{S}(undef, length(array(cpa1)) + length(array(cpa2)))
+    result[blocks1] = array(cpa1)
+    result[blocks2] = array(cpa2)
+    return CartesianProductArray(result)
+end
+
 """
     reach(problem, options)
 
@@ -53,7 +87,6 @@ function reach_mixed(problem::Union{IVP{<:CLDS{NUM}, <:LazySet{NUM}},
     partition = convert_partition(options[:partition])
     T = options[:T]
     N = (T == Inf) ? nothing : ceil(Int, T / options[:δ])
-    guards_proj = options[:guards_proj]
     # Cartesian decomposition of the initial set
     if length(partition) == 1 && length(partition[1]) == n &&
             options[:block_options_init] == LinearMap
@@ -170,9 +203,8 @@ function reach_mixed(problem::Union{IVP{<:CLDS{NUM}, <:LazySet{NUM}},
         invariant = LazySets.Approximations.project(invariant, vars)
     end
     termination = get_termination_function_out(N, invariant)
-    block_options = options[:block_options_init]
-    push!(args, guards_proj)
-    push!(args, block_options)
+    push!(args, options[:guards_proj])
+    push!(args, options[:block_options_init])
     push!(args, vars)
     push!(args, termination)
 
@@ -184,7 +216,7 @@ function reach_mixed(problem::Union{IVP{<:CLDS{NUM}, <:LazySet{NUM}},
         nothing
     push!(args, progress_meter)
 
-    # choose algorithm backend
+    # preallocated result
     push!(args, res)
 
     # call the adequate function with the given arguments list

src/ReachSets/ReachSets.jl

@@ -115,8 +115,6 @@ available_algorithms = Dict{String, Dict{String, Any}}()
 # "explicit" backends
 push!(available_algorithms, "explicit_blocks"=>Dict("func"=>reach_blocks!,
                                                     "is_explicit"=>true))
-push!(available_algorithms, "explicit_blocks_mixed"=>Dict("func"=>reach_blocks!,
-                                                    "is_explicit"=>true))
 
 push!(available_algorithms,
       "wrap"=>Dict("func"=>reach_blocks_wrapping_effect!,