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)
Currently for hybrid systems we have a waiting list of flowpipes to analyze and just
popthe next element.https://github.com/JuliaReach/Reachability.jl/blob/870a0c4f431fa6d59627c6530ccd80184e5615bd/src/solve.jl#L153
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: