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
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
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.