22 #include <spot/twaalgos/emptiness.hh>
23 #include <spot/twaalgos/sccinfo.hh>
24 #include <spot/misc/bitvect.hh>
140 SPOT_API std::vector<bool>
An acceptance condition.
Definition: acc.hh:62
A bit vector.
Definition: bitvect.hh:52
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:443
void generic_emptiness_check_select_version(const char *emversion=nullptr)
bool accepting_transitions_scc(const scc_info &si, unsigned scc, const acc_cond aut_acc, acc_cond::mark_t removed_colors, std::vector< bool > &accepting_transitions, const bitvect &kept)
bool generic_emptiness_check_for_scc(const scc_info &si, unsigned scc)
Emptiness check of one SCC, for any acceptance condition.
twa_run_ptr generic_accepting_run(const const_twa_graph_ptr &aut)
Accepting run search in an automaton, for any acceptance condition.
bool generic_emptiness_check(const const_twa_graph_ptr &aut)
Emptiness check of an automaton, for any acceptance condition.
std::vector< bool > accepting_transitions(const const_twa_graph_ptr aut, acc_cond cond)
bool maximal_accepting_loops_for_scc(const scc_info &si, unsigned scc, const acc_cond &forced_acc, const bitvect &keep, std::function< void(const scc_info &, unsigned)> callback)
Compute set of maximal accepting loops in one SCC, for any acceptance condition.
Definition: automata.hh:27
An acceptance mark.
Definition: acc.hh:85