21#include <spot/twaalgos/emptiness.hh>
22#include <spot/twaalgos/sccinfo.hh>
23#include <spot/misc/bitvect.hh>
139 SPOT_API std::vector<bool>
An acceptance condition.
Definition: acc.hh:61
A bit vector.
Definition: bitvect.hh:51
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:449
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)
std::vector< bool > accepting_transitions(const const_twa_graph_ptr aut, acc_cond cond)
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.
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:26
An acceptance mark.
Definition: acc.hh:84