Add a fallback to the fully symbolic attractor detection if the NFVS search fails #123
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is very straightforward: if the NFVS method produces more than
attractor_candidates_limit
candidate states, fall back to basic symbolic search using AEON.This is not very common (hence I added an optional flag to enable this behavior which is off by default), but it does help with a few variants of model
002
and079
where we would otherwise just get stuck on enumerating the attractor candidate states. However, it may be necessary to manually decrease theattractor_candidates_limit
to get the full performance benefit (enumerating 100_000 candidates, which is the default, still takes a lot of time).