Scheduling of flowpipes

[schillic]

Currently for hybrid systems we have a waiting list of flowpipes to analyze and just pop the next element.

Reachability.jl/src/solve.jl

Line 153 in 870a0c4

loc_id, X0, jumps = pop!(waiting_list)

Generally we should allow more control here by letting a scheduler decide which flowpipe to analyze next.

This enables (guided or unguided) search for violations as well as establishing bounded safety in incremental stages. Note that the order actually affects the total runtime: a flowpipe that covers a large part of the state space can make other flowpipes redundant. Possible strategies are:

• prefer big sets
• prefer flowpipes that potentially eliminate many other flowpipes in the waiting list
• prefer certain locations in the automaton (e.g., because they are easier to analyze or because they are closer to an error location)
• prefer lower time frames
• prefer shorter paths
• explore new locations first