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_map
s 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
ReachSet
s (suggested name:SparseReachSet
) using type composition. - We add a
project
function with methods forReachSet
andSparseReachSet
which, given a list of dimensions, returns a set projected to those dimensions. Dimension0
for time is possible.