Adding BFFPS19 CPost and Decomposed Hybrid algorithms

[kpotomkin]

(Follow-up work was deferred to #656.)

Still to resolve:

• Add tests, in particular where the blocks of interest are not connected and do not start with dimension x1.
• Check why :overapproximation is ignored in clustering.
• Address double termination check.

Future work:

• Add internal options as a separate field to the post operators.

[schillic]

I have not yet looked at the algorithms. It is hard to review because I do not see the changes here.
Did you not say that there were problems with the function names? How did you resolve them?

[kpotomkin]

Did you not say that there were problems with the function names?

Yes, I had these problems.

How did you resolve them?

I renamed some methods (see termination methods). Regarding reach_blocks: The problem was solved thanks to having different signature in comparison with reach_blocks in BFFPSV18. In particular, I have added constraints_list (from the guard), blocks approximations option and vars. Moreover, I divided these algorithms, so they cannot be called from wrong CPost (see here)).
Regarding choosing correct reach function: it was fixed thanks to renaming here

[schillic]

I omitted reach_blocks.jl and the discrete post for now.

[schillic]

What do you mean here?

[kpotomkin]

Somehow user-defined :overapproximation doesn't work in clustering function. It always overapproximate ConvexHull with Hyperrectangular.

[schillic]

I looked at the "sparse" algorithm only, but I assume that the same comments apply in the dense case.

[mforets]

A comment regarding the tests. I've ran test/Reachability/models and:

• bouncing ball works
• thermostat breaks with the following missing function:

julia> sol = solve(system, options, opC, DecomposedDiscretePost());
[info] Reachable States Computation...
[info] Time discretization...
[info] elapsed time: 4.220e-04 seconds
[info] - Decomposing X0
[info] elapsed time: 1.717e-05 seconds
[info] - Computing successors
ERROR: MethodError: no method matching overapproximate(::EmptySet{Float64}, ::Type{CartesianProductArray}, ::Array{Type{#s127} w
here #s127<:LazySet,1})
Closest candidates are:
  overapproximate(::Intersection{N,#s84,#s63} where #s63<:AbstractPolyhedron{N} where #s84<:(CartesianProductArray{N,S} where S<
:LazySet{N}), ::Type{CartesianProductArray}, ::Any) where N at /Users/forets/.julia/dev/LazySets/src/Approximations/overapproxim
ate.jl:951
  overapproximate(::Intersection{N,#s84,#s63} where #s63<:(CartesianProductArray{N,S} where S<:LazySet{N}) where #s84<:AbstractP
olyhedron{N}, ::Type{CartesianProductArray}, ::Any) where N at /Users/forets/.julia/dev/LazySets/src/Approximations/overapproxim
ate.jl:971
  overapproximate(::S<:LazySet, ::Type{S<:LazySet}, ::Any...) where S<:LazySet at /Users/forets/.julia/dev/LazySets/src/Approxim
ations/overapproximate.jl:18
  ...
Stacktrace:
 [1] getX_store at /Users/forets/.julia/dev/Reachability/src/ReachSets/ContinuousPost/BFFPS19/reach_blocks.jl:9 [inlined]
 [2] reach_blocks!(::Array{Float64,2}, ::Array{LazySet{Float64},1}, ::ConstantInput{MinkowskiSum{Float64,LazySets.LinearMap{Floa
t64,Singleton{Float64,Array{Float64,1}},Float64,Array{Float64,2}},Hyperrectangle{Float64}}}, ::Function, ::getfield(Reachability
.ReachSets, Symbol("##81#87")), ::Int64, ::Int64, ::Nothing, ::Array{Int64,1}, ::Array{Int64,1}, ::Float64, ::Array{HalfSpace{Fl
oat64,Array{Float64,1}},1}, ::Array{Type{#s127} where #s127<:LazySet,1}, ::Array{Int64,1}, ::getfield(Reachability.ReachSets, Sy
mbol("##97#98")){Int64,HalfSpace{Float64,Array{Float64,1}}}, ::ProgressMeter.Progress, ::Array{ReachSet{CartesianProductArray{Fl
oat64,LazySet{Float64}},Float64},1}) at /Users/forets/.julia/dev/Reachability/src/ReachSets/ContinuousPost/BFFPS19/reach_blocks.
jl:247
 [3] macro expansion at /Users/forets/.julia/dev/Reachability/src/ReachSets/ContinuousPost/BFFPS19/reach.jl:212 [inlined]
 [4] reach_mixed(::InitialValueProblem{ConstrainedLinearControlDiscreteSystem{Float64,Array{Float64,2},IdentityMultiple{Float64}
,HalfSpace{Float64,Array{Float64,1}},ConstantInput{MinkowskiSum{Float64,LazySets.LinearMap{Float64,Singleton{Float64,Array{Float
64,1}},Float64,Array{Float64,2}},Hyperrectangle{Float64}}}},ConvexHull{Float64,Singleton{Float64,Array{Float64,1}},MinkowskiSum{
Float64,MinkowskiSum{Float64,MinkowskiSum{Float64,LazySets.LinearMap{Float64,Singleton{Float64,Array{Float64,1}},Float64,Array{F
loat64,2}},LazySets.LinearMap{Float64,Singleton{Float64,Array{Float64,1}},Float64,Array{Float64,2}}},Hyperrectangle{Float64}},Hy
perrectangle{Float64}}}}, ::Reachability.TwoLayerOptions) at /Users/forets/.julia/dev/Reachability/src/ReachSets/ContinuousPost/
BFFPS19/reach.jl:211
 [5] reach_mixed(::InitialValueProblem{ConstrainedLinearControlContinuousSystem{Float64,Array{Float64,2},IdentityMultiple{Float6
4},HalfSpace{Float64,Array{Float64,1}},ConstantInput{LazySets.LinearMap{Float64,Singleton{Float64,Array{Float64,1}},Float64,Arra
y{Float64,2}}}},Singleton{Float64,Array{Float64,1}}}, ::Reachability.TwoLayerOptions) at /Users/forets/.julia/dev/Reachability/s
rc/ReachSets/ContinuousPost/BFFPS19/reach.jl:235
 [6] macro expansion at /Users/forets/.julia/dev/Reachability/src/ReachSets/ContinuousPost/BFFPS19/BFFPS19.jl:249 [inlined]
 [7] post(::BFFPS19, ::InitialValueProblem{ConstrainedLinearControlContinuousSystem{Float64,Array{Float64,2},IdentityMultiple{Fl
oat64},HalfSpace{Float64,Array{Float64,1}},ConstantInput{LazySets.LinearMap{Float64,Singleton{Float64,Array{Float64,1}},Float64,
Array{Float64,2}}}},Singleton{Float64,Array{Float64,1}}}, ::Options) at /Users/forets/.julia/dev/Reachability/src/ReachSets/Cont
inuousPost/BFFPS19/BFFPS19.jl:248
 [8] #solve!#40(::BFFPS19, ::Function, ::InitialValueProblem{ConstrainedLinearControlContinuousSystem{Float64,Array{Float64,2},A
rray{Float64,2},HalfSpace{Float64,Array{Float64,1}},ConstantInput{Singleton{Float64,Array{Float64,1}}}},Singleton{Float64,Array{
Float64,1}}}, ::Options) at /Users/forets/.julia/dev/Reachability/src/solve.jl:74
 [9] (::getfield(Reachability, Symbol("#kw##solve!")))(::NamedTuple{(:op,),Tuple{BFFPS19}}, ::typeof(Reachability.solve!), ::Ini
tialValueProblem{ConstrainedLinearControlContinuousSystem{Float64,Array{Float64,2},Array{Float64,2},HalfSpace{Float64,Array{Floa
t64,1}},ConstantInput{Singleton{Float64,Array{Float64,1}}}},Singleton{Float64,Array{Float64,1}}}, ::Options) at ./none:0
 [10] solve!(::InitialValueProblem{HybridSystem{LightAutomaton{LightGraphs.SimpleGraphs.SimpleDiGraph{Int64},LightGraphs.SimpleG
raphs.SimpleEdge{Int64}},ConstrainedLinearControlContinuousSystem{Float64,Array{Float64,2},Array{Float64,2},HalfSpace{Float64,Ar
ray{Float64,1}},ConstantInput{Singleton{Float64,Array{Float64,1}}}},ConstrainedIdentityMap{HalfSpace{Float64,Array{Float64,1}}},
AutonomousSwitching,Array{ConstrainedLinearControlContinuousSystem{Float64,Array{Float64,2},Array{Float64,2},HalfSpace{Float64,A
rray{Float64,1}},ConstantInput{Singleton{Float64,Array{Float64,1}}}},1},Array{ConstrainedIdentityMap{HalfSpace{Float64,Array{Flo
at64,1}}},1},Array{AutonomousSwitching,1}},Array{Tuple{Int64,Singleton{Float64,Array{Float64,1}}},1}}, ::Options, ::BFFPS19, ::D
ecomposedDiscretePost) at /Users/forets/.julia/dev/Reachability/src/solve.jl:173
 [11] solve(::InitialValueProblem{HybridSystem{LightAutomaton{LightGraphs.SimpleGraphs.SimpleDiGraph{Int64},LightGraphs.SimpleGr
aphs.SimpleEdge{Int64}},ConstrainedLinearControlContinuousSystem{Float64,Array{Float64,2},Array{Float64,2},HalfSpace{Float64,Arr
ay{Float64,1}},ConstantInput{Singleton{Float64,Array{Float64,1}}}},ConstrainedIdentityMap{HalfSpace{Float64,Array{Float64,1}}},A
utonomousSwitching,Array{ConstrainedLinearControlContinuousSystem{Float64,Array{Float64,2},Array{Float64,2},HalfSpace{Float64,Ar
ray{Float64,1}},ConstantInput{Singleton{Float64,Array{Float64,1}}}},1},Array{ConstrainedIdentityMap{HalfSpace{Float64,Array{Floa
t64,1}}},1},Array{AutonomousSwitching,1}},Array{Tuple{Int64,Singleton{Float64,Array{Float64,1}}},1}}, ::Options, ::BFFPS19, ::De
composedDiscretePost) at /Users/forets/.julia/dev/Reachability/src/solve.jl:101
 [12] top-level scope at none:0

[mforets]

Suggested change

	if reach_set_intersected isa EmptySet
	if isempty(reach_set_intersected)
	break
	end

or even isempty(reach_set_intersected) && break (same in the other places).

[schillic]

Okay since we always operate on bounded sets and the emptiness information is given in the type. Generally isempty is more costly.

[mforets]

The termination makes an isempty check (see eg. termination_inv_out), and a new isempty check is made here. This is intended? Why not using the first output argument (terminate) here?

[schillic]

The termination makes an isempty check

Not always. You can also terminate by bounding the number of steps.

[mforets]

Hmm and you can't use the second argument, skip? What is the purpose of these checks? Adding documentation would help the maintainability of this code :)

[kpotomkin]

Should I squash the commits?

[mforets]

Either way is good; we can squash just before merging.

Can you add the new continuous post and discrete post to the hybrid tests?

[schillic]

We are not done here (build is failing, tests are missing).

[mforets]

This PR should be updated accordingly to #647

[mforets]

Are we done here?

[schillic]

Are we done here?

The missing items are collected in the first comment. But we just agreed to merge and open a follow-up issue.

[schillic]

The remaining tasks can be addressed in a follow-up issue.