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 and 079 where we would otherwise just get stuck on enumerating the attractor candidate states. However, it may be necessary to manually decrease the attractor_candidates_limit to get the full performance benefit (enumerating 100_000 candidates, which is the default, still takes a lot of time).
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).