You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The find_path algorithm does preliminary checks using the is_trivially_unreachable function in reachability.rs
Currently, these checks are very limited.
More could be added, which would:
Help improve performance, by avoiding to explore the entire state space in cases the end state is unreachable and it can be caught with a preliminary check instead
Help allow better responses for why the end state is unreachable, see #136
We dont have a full overview of what checks could be done, but one big and interesting idea is checking each component individually first.
In a combined transition system, if the end state is not reachable in the individual components, then it is also not reachable in the combined system.
Doing this will be cheaper compared to exploring the combined system, and will also allow error messages such as "Not reachable in component Machine" instead of just saying its not reachable at all.
The text was updated successfully, but these errors were encountered:
The find_path algorithm does preliminary checks using the is_trivially_unreachable function in reachability.rs
Currently, these checks are very limited.
More could be added, which would:
Help improve performance, by avoiding to explore the entire state space in cases the end state is unreachable and it can be caught with a preliminary check instead
Help allow better responses for why the end state is unreachable, see #136
We dont have a full overview of what checks could be done, but one big and interesting idea is checking each component individually first.
In a combined transition system, if the end state is not reachable in the individual components, then it is also not reachable in the combined system.
Doing this will be cheaper compared to exploring the combined system, and will also allow error messages such as "Not reachable in component Machine" instead of just saying its not reachable at all.
The text was updated successfully, but these errors were encountered: