Better errors from find_path when a preliminary check fails
Open
- Dominant language
- Rust
- Stars
- 4
- Forks
- 6
- PR merge metrics
- No merged PRs in 30d
Description
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
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.