accessibility properties
We just discussed with @max and @aga the fact that some algorithms call scc_filter()
as a preprocessing step, some don't. For instance currently tgba_determinize()
calls scc_filter()
only if simulation-based reductions are activated, and it is unclear why this this done only in this case.
It might be interesting to add a property recording whether an automaton has been trimmed, in order to skip duplicate calls to such a function. I would suggest to use two properties: accessible
(all states are reachable from initial state) and coaccessible
(all states can reach some accepting cycle). accessible
would for instance be set by purge_unreachable_states()
, and both properties would be set by scc_filter_states()
and similar functions. Note that is_empty()
can simplified when run on automata that are both accessible
and coaccessible
, but I figure this is unlikely to be very useful in practice.
One issue is that these proposed properties are not always enough to decide if scc_filter()
can be skipped, because scc_filter()
does more than just removing useless states: it also simplifies the acceptance sets in each SCC.