JuliaReach/Reachability.jl

Replace inout_map by low-dimensional flowpipes

schillic opened this issue · 1 comments

Example

Say that you want to plot dimensions x3 and x4 and you do a decomposed analysis only for those two dimensions. Then the result will be a 2D flowpipe representing x3 and x4. However, the projection would try to access dimensions 3 and 4 (because those were the specified dimensions), which do not exist in a 2D flowpipe.

Current state

Internally we create inout_maps to map to the correct dimensions. But this is poorly integrated and at some places we just inject them.

Proposal

Let the ReachSet automatically handle these situations. They should receive the information which dimensions are stored and which of them are just taken as universal. (This is essentially what was proposed in #275.) Essentially this internal information is equivalent to the inout_map, but we can remove some hacks.

Result of a discussion with @mforets:

  • We add a new type for low-dimensional ReachSets (suggested name: SparseReachSet) using type composition.
  • We add a project function with methods for ReachSet and SparseReachSet which, given a list of dimensions, returns a set projected to those dimensions. Dimension 0 for time is possible.