Follow-up work of BFFPS19
schillic opened this issue · 2 comments
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:
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 andoverapproximation
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])
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
.