|
typedef std::vector< unsigned > | scc_succs |
|
|
| scc_info (const_twa_graph_ptr aut) |
|
const_twa_graph_ptr | get_aut () const |
|
unsigned | scc_count () const |
|
bool | reachable_state (unsigned st) const |
|
unsigned | scc_of (unsigned st) const |
|
auto | begin () const SPOT_RETURN(node_.begin()) |
|
auto | end () const SPOT_RETURN(node_.end()) |
|
auto | cbegin () const SPOT_RETURN(node_.cbegin()) |
|
auto | cend () const SPOT_RETURN(node_.cend()) |
|
auto | rbegin () const SPOT_RETURN(node_.rbegin()) |
|
auto | rend () const SPOT_RETURN(node_.rend()) |
|
const std::vector< unsigned > & | states_of (unsigned scc) const |
|
unsigned | one_state_of (unsigned scc) const |
|
unsigned | initial () const |
| Get number of the SCC containing the initial state. More...
|
|
const scc_succs & | succ (unsigned scc) const |
|
bool | is_trivial (unsigned scc) const |
|
acc_cond::mark_t | acc (unsigned scc) const |
|
bool | is_accepting_scc (unsigned scc) const |
|
bool | is_rejecting_scc (unsigned scc) const |
|
void | determine_unknown_acceptance () |
|
bool | is_useful_scc (unsigned scc) const |
|
bool | is_useful_state (unsigned st) const |
|
std::vector< std::set
< acc_cond::mark_t > > | used_acc () const |
| Return the set of all used acceptance combinations, for each accepting SCC. More...
|
|
std::set< acc_cond::mark_t > | used_acc_of (unsigned scc) const |
|
acc_cond::mark_t | acc_sets_of (unsigned scc) const |
|
std::vector< bool > | weak_sccs () const |
|
bdd | scc_ap_support (unsigned scc) const |
|
|
void | determine_usefulness () |
|
const scc_node & | node (unsigned scc) const |
|
|
std::vector< unsigned > | sccof_ |
|
std::vector< scc_node > | node_ |
|
const_twa_graph_ptr | aut_ |
|
unsigned spot::scc_info::initial |
( |
| ) |
const |
|
inline |
Get number of the SCC containing the initial state.
Return the set of all used acceptance combinations, for each accepting SCC.
The documentation for this class was generated from the following file: