search

JuliaReach / Reachability.jl

Reachability and Safety of Nondeterministic Dynamical Systems
MIT License
50 stars 4 forks source link

Adding BFFPS19 CPost and Decomposed Hybrid algorithms #641

Closed kpotomkin closed 5 years ago

kpotomkin commented 5 years ago

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

Still to resolve:

Future work:

kpotomkin commented 5 years ago

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

mforets commented 5 years ago

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

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
kpotomkin commented 5 years ago

Should I squash the commits?

mforets commented 5 years ago

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 commented 5 years ago

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

mforets commented 5 years ago

This PR should be updated accordingly to https://github.com/JuliaReach/Reachability.jl/pull/647

mforets commented 5 years ago

Are we done here?

schillic commented 5 years ago

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.