Closed schillic closed 4 years ago
a ReachSet must always be high dimensional).
i guess you mean full dimensional
There's also the related issue https://github.com/JuliaReach/Reachability.jl/issues/541 but we can do on a follow-up PR.
This changeset does not work with the way we implemented the hybrid algorithm. We need to discuss this.
The last commit solved it again. It is certainly a workaround but I think overall the state has improved :smiley:
Closes #668.
Summary:
SparseReachSet
which behaves like aReachSet
but additionally stores the dimensions in which it was computed (from now on, aReachSet
must always be high dimensional).AbstractReachSet
forReachSet
andAbstractReachSet
with the methodsset
,time_start
,time_end
, andproject
. Theproject
method just receives a projection matrix.SparseReachSet
flowpipes, which consists of two steps:compute_dimensions
to compute the dimensions forSparseReachSet
s (currently this function resides inBFFPSV18
).SparseReachSet
s.project
/project_reach
:AbstractReachSet
individually.CartesianProduct
with the time interval.inout_map
from reachability algorithms (it still exists for properties, which can maybe be refactored another time).Some of the benchmarks in https://github.com/JuliaReach/ReachabilityBenchmarks need to be updated (because we access some
ReachSet
fields explicitly :-1:).