21#include <spot/twaalgos/sccinfo.hh>
22#include <spot/twa/twagraph.hh>
105 SPOT_API std::vector<bool>
123 count_univbranch_states(
const const_twa_graph_ptr& aut);
139 count_univbranch_edges(
const const_twa_graph_ptr& aut);
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:449
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
bool is_deterministic(const const_twa_graph_ptr &aut)
Return true iff aut is deterministic.
unsigned count_nondet_states(const const_twa_graph_ptr &aut)
Count the number of states with non-deterministic branching in aut.
void highlight_nondet_edges(twa_graph_ptr &aut, unsigned color)
Highlight nondeterministic edges.
void highlight_nondet_states(twa_graph_ptr &aut, unsigned color)
Highlight nondeterministic states.
Definition: automata.hh:26
void highlight_semidet_sccs(scc_info &si, unsigned color)
Highlight the deterministic part of the automaton.
bool is_complete(const const_twa_graph_ptr &aut)
Return true iff aut is complete.
bool is_semi_deterministic(const const_twa_graph_ptr &aut)
Return true iff aut is semi-deterministic.
void check_determinism(twa_graph_ptr aut)
Set the deterministic and semi-deterministic properties appropriately.
std::vector< bool > semidet_sccs(scc_info &si)
Whether an SCC is in the deterministic part of an automaton.