Bouncing ball model with GLGM06

[mforets]

function bouncing_ball()
    automaton = LightAutomaton(1)
    A = [0.0 1.0; 0.0 0.0]
    B = reshape([0.0, -1.0], (2, 1))
    U = Singleton([1.0])
    inv = HalfSpace([-1.0, 0.0], 0.0) # x >= 0
    m1 = ConstrainedLinearControlContinuousSystem(A, B, inv, ConstantInput(U))
    modes = [m1]

    # transition from m1 to m1 (self-loop)
    add_transition!(automaton, 1, 1, 1)
    A = [1.0 0.0; 0.0 -0.75]
    guard = HPolyhedron([HalfSpace([0.0, 1.0], 0.0),   # v ≤ 0
                         HalfSpace([-1.0, 0.0], 0.0),  # x ≥ 0
                         HalfSpace([1.0, 0.0], 0.0)])  # x ≤ 0
    t1 = ConstrainedLinearMap(A, guard)

    # transition annotations
    resetmaps = [t1]

    # switching
    switchings = [AutonomousSwitching()]

    ℋ = HybridSystem(automaton, modes, resetmaps, switchings)

    # initial condition in mode 1
    X0 = Hyperrectangle(low=[10.0, 0.0], high=[10.2, 0.0])
    initial_condition = [(1, X0)]

    system = InitialValueProblem(ℋ, initial_condition)

    options = Options(:mode=>"reach", :T=>6.0, :plot_vars=>[1, 2], :project_reachset=>false)

    return (system, options)
end
problem, options = bouncing_ball();

solve(problem, options, BFFPSV18(:δ=>0.1), LazyDiscretePost());

plot(sol_BFFPSV18, use_subindices=false, aspectratio=1, alpha=.5, color=:lightblue)

options = Options(:mode=>"reach", :T=>5.0, :plot_vars=>[1, 2], :project_reachset=>false)

@time sol_GLGM06 = solve(problem, options, GLGM06(:δ=>0.1), LazyDiscretePost());

plot(sol_BFFPSV18, use_subindices=false, aspectratio=1, alpha=.5, color=:lightblue)

---

the intersection is empty

Stacktrace:
 [1] error(::String) at ./error.jl:33
 [2] #ρ_helper#148(::Base.Iterators.Pairs{Union{},Union{},Tuple{},NamedTuple{(),Tuple{}}}, ::Function, ::Array{Float64,1}, ::Intersection{Float64,CartesianProductArray{Float64,Zonotope{Float64}},HalfSpace{Float64}}, ::String) at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:261
 [3] ρ_helper at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:256 [inlined]
 [4] #ρ#149 at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:377 [inlined]
 [5] ρ at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:377 [inlined]
 [6] box_approximation_helper at /Users/forets/.julia/dev/LazySets/src/Approximations/box_approximations.jl:126 [inlined]
 [7] box_approximation(::Intersection{Float64,CartesianProductArray{Float64,Zonotope{Float64}},HalfSpace{Float64}}) at /Users/forets/.julia/dev/LazySets/src/Approximations/box_approximations.jl:27
 [8] overapproximate(::Intersection{Float64,CartesianProductArray{Float64,Zonotope{Float64}},HalfSpace{Float64}}, ::Type{Hyperrectangle}) at /Users/forets/.julia/dev/LazySets/src/Approximations/overapproximate.jl:84
 [9] tube⋂inv!(::LazyDiscretePost, ::Array{ReachSet{CartesianProductArray{Float64,Zonotope{Float64}},Float64},1}, ::HalfSpace{Float64}, ::Array{ReachSet{LazySet{Float64},Float64},1}, ::Array{Float64,1}) at /Users/forets/.julia/dev/Reachability/src/ReachSets/DiscretePost/LazyDiscretePost.jl:102

[mforets]

Since GLGM06 currently does not take intersections with the invariant, one has to pass this option to the discrete post: LazyDiscretePost(:check_invariant_intersection=>true).

Using #580 and #581, then bball works with GLGM06.

options = Options(:mode=>"reach", :T=>5.0, :plot_vars=>[1, 2])

@time sol_GLGM06 = solve(problem, options, GLGM06(:δ=>0.1), LazyDiscretePost(:check_invariant_intersection=>true));

plot(sol_GLGM06, use_subindices=false, aspectratio=1, alpha=.5, color=:lightblue)