JuliaReach/Reachability.jl

Follow-up work of BFFPS19

schillic opened this issue · 2 comments

Quoting from #641:

Still to resolve:

Future work:

Check why :overapproximation is ignored in clustering. - works.
To make it work we need to be sure that the following options are on:

  • partitioning option allows to have specified overapproximation. For instance, we need 2-dim block for OctDirections;
  • we need to pass block_options to continuous solver and overapproximation to discrete solver to have correct overapproximation. Maybe we should add a general option for the problem, which will pass specific overapproximation to the solvers.

we need to pass overapproximation to discrete solver

Yeah, obviously 😉

we need to pass block_options to continuous solver

I do not see why. The clustering happens in the discrete-post operator. block_options should only affect the precision of the sets that are the input to the clustering. Can you try with block_options -> Hyperrectangle and overapproximation -> OctDirections and see if it is the same as for overapproximation -> Hyperrectangle? Then that would be a bug.

Here is what I expect should happen (only using LazySets):

using LazySets, Plots
using LazySets: translate

O1 = overapproximate(rand(Ball2), OctDirections)
O2 = translate(O1, [1., 1.])
H1 = overapproximate(O1, Hyperrectangle)
H2 = overapproximate(O2, Hyperrectangle)
CH1 = overapproximate(ConvexHull(H1, H2), Hyperrectangle)
CO1 = overapproximate(ConvexHull(H1, H2), OctDirections)
CH2 = overapproximate(ConvexHull(O1, O2), Hyperrectangle)
CO2 = overapproximate(ConvexHull(O1, O2), OctDirections)

plot([O1, O2, H1, H2])
plot!([CH1, CH2, CO1, CO2])

1
2

Using OctDirections for clustering produces the diagonal sets. The diagonal for two octagons is more precise than the diagonal for two boxes. On the other hand, using Hyperrectangle for clustering produces the same box irrespective of block_options.