search

JuliaReach / Reachability.jl

Reachability and Safety of Nondeterministic Dynamical Systems
MIT License
50 stars 4 forks source link

Sets after jump become bigger although they were smaller before #328

Closed schillic closed 6 years ago

schillic commented 6 years ago

Example: filtered oscillator Even though the jump starting from the purple reach tube should land in a subset of the green reach tube (which was the jump target from the orange reach tube), we obtain the blue reach tube.

fo_after_jump

schillic commented 6 years ago

This is what happens if we deactivate clustering for the second round. It does not look smaller than the first round, but also at least not bigger.

fo_no_clustering

Here are two sample successor reach tubes (clustering deactivated).

fo_no_clustering_samples

schillic commented 6 years ago

Filtered oscillator, ApproximatingDiscretePost:

plot(sol) # whole flowpipe
plot!(Reachability.ReachSolution(sol.Xk[1:137], Options(:plot_vars=>[1,2])), opacity=0.5) # first reach tube
plot!(Reachability.ReachSolution(sol.Xk[348:483], Options(:plot_vars=>[1,2])), opacity=0.5) # fifth reach tube
plot!(Reachability.ReachSolution(sol.Xk[138:138], Options(:plot_vars=>[1,2])), opacity=0.5) # successor of first reach tube
plot!(Reachability.ReachSolution(sol.Xk[484:484], Options(:plot_vars=>[1,2])), opacity=0.5) # successor of fifth reach tube

As we can see, the successor of the smaller set is bigger than the successor of the bigger set.

fo_after_jump_1

Also, notice that the sets are shifted to the top. I expected that the rectangles contain the end of the reach tube because here we do not have any assignments.