find_path uses is_trivially_unreachable to stop early if these preliminary checks show it is trivially unreachable.
Currently there are few preliminary checks, but more can be added, see #135
Each of these cases could report a specific response, giving the user more precise information on why it is not reachable.
For example, could say ""end state" is not reachable because the given clock constraints do not intersect with the invariant of the end state", or something along those lines
find_path uses is_trivially_unreachable to stop early if these preliminary checks show it is trivially unreachable.
Currently there are few preliminary checks, but more can be added, see #135
Each of these cases could report a specific response, giving the user more precise information on why it is not reachable. For example, could say ""end state" is not reachable because the given clock constraints do not intersect with the invariant of the end state", or something along those lines