JuliaReach
Property verified on larger input box, but may be violated on strict subset [SpacecraftDocking]
When running SpacecraftDocking on the default input set X₀ = Hyperrectangle(low=[70, 70, -0.14, -0.14], high=[106, 106, 0.14, 0.14]), verified is returned. Surprisingly (to me), when reducing the input set to X₀ = Hyperrectangle(low=[70.0, 70.0, -0.14, -0.14],high=[80, 80, -0.1, -0.1],) may be violated gets returned.
I'm curious why this could be the case, and if this is a bug, as I would expect a subset of the original set to be easier to verify.
To reproduce: clone the repo and run 'SpacecraftDocking.jl' with the two different input sets; nothing else was changed.
Additionally, one of the simulations appears to be outside the yellow (overapproximated?) region when examining the returned .png.
.toml: Project.txt
You are right that this is wrong. Specifically, the issue is that the variables for dimensions 3 and 4 are not updated correctly for the original set (left plot). They are updated correctly for your reduced set (right plot).
We are aware of a bug in the TaylorModels algorithm, but we cannot fix it. I presume it happens here if 0 is included in the initial set for dimensions 3 and 4 (which is not the case for your updated initial set).
(FWIW, the investigation also uncovered another bug in the specification.)
Thank you very much for the fast answer! Is there a correct/reasonable way to work around the bug in the TaylorModels, or must I use a different framework? If I always exclude 0, should no bug occur?
If I always exclude 0, should no bug occur?
This was only speculation. Nobody knows the root cause of the bug (main reason why it is not fixed). So I unfortunately cannot give you a workaround. My best advice is to avoid models where this problem occurs; if you have to use the model, look at the plot and compare to the simulations.