Make Gearbox benchmark succeed

[schillic]

• The reachability analysis terminates quickly for 10% of the time horizon (i.e., :T=>0.05 instead of :T=>0.5) :+1:, but runs (seemingly) forever even for :T=>0.1 :-1: Other tools report runtimes of less than 0.3 seconds for the whole time horizon. I suspect that the problem comes from the self-loops; this requires some thinking.
• For :T=>0.05, plots look good for the variables x3/x4 compared to the other plots. When I look at the plots of t/x5, there are three different flowpipes already - not sure if that is correct or not.
• The property checking is fast :+1:, but only because the property is violated quickly :-1: So we also need to increase precision at some point.
• There are some TODOs in the model code, mostly where the model deviates from the SpaceEx model. They might be related.

Originally posted by @schillic in https://github.com/JuliaReach/ReachabilityBenchmarks/pull/72#issuecomment-470852699

[schillic]

Some comments:

• The main problem is the self-loop transition t2. (When omitting that transition, the analysis terminates quickly.) We seem to repeat the analysis for the same time step, effectively not moving forward. Since the fixpoint check does not prevent this, the set of states must change (probably grows) every time. When bounding the number of jumps (:max_jumps) to two or three, this growth can be seen.
• Using the invariant from the SpaceEx model does not seem to help.

  invariant = HPolyhedron([HalfSpace(sparsevec([px], [1.], n), Δp),
                           HalfSpace(sparsevec([px, py], [tan(θ), 1.], n), 0.),
                           HalfSpace(sparsevec([px, py], [tan(θ), -1.], n), 0.)])

• Clustering adds a lot of approximation error here. Using :clustering => :none_oa does not really help, though. EDIT: It does for smaller time steps, see the plots two comments below.
• Using the ConcreteDiscretePost requires CDDLib, but even then does not help.

[schillic]

One idea for the problem with repeating the same time step is to consider the time variable in the model. When the interval domain of that variable is disjoint from the time interval of the ReachSet, I think we can conclude that the set is spurious and drop it. I do not know if this happens here, though.

[schillic]

The following settings give a good start (very slow, but the plot looks good). However, after the second transition, things explode (probably due to the deactivated clustering).

    opC = BFFPSV18(:δ => 0.0001, :partition => [1:5, 6:6], :lazy_inputs_interval => -1)
    opD = LazyDiscretePost(:lazy_R⋂I => true, :lazy_R⋂G => false)
    options[:max_jumps] = 2
    options[:clustering] = :none_oa
    options[:mode] = "reach"
    options[:plot_vars] = [3, 4]
    options[:project_reachset] = true

When using opD = ConcreteDiscretePost(), the results get even better (and the analysis is only slightly slower):

My conclusion is that we need a better clustering algorithm and more precise overapproximation in the discrete part (or use polyhedra) for this model.

We can run the ConcreteDiscretePost for three jumps in a couple of minutes (I used :δ => 0.0002 here) (after fixing some problems with overapproximations of sets becoming empty sets):