Follow-up work of BFFPS19

[schillic]

Quoting from #641:

Still to resolve:

• Add tests, in particular where the blocks of interest are not connected and do not start with dimension x1.
• Check why :overapproximation is ignored in clustering.
• Address double termination check.
• add option for lazy/concrete intersection (maybe resolve #693 first)

Future work:

• Add internal options as a separate field to the post operators.

[kpotomkin]

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.

[schillic]

we need to pass overapproximation to discrete solver

Yeah, obviously :wink:

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])

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.