spot
2.3.1
|
Compute an SCC map and gather assorted information. More...
#include <spot/twaalgos/sccinfo.hh>
Classes | |
class | scc_node |
Public Types | |
typedef std::vector< unsigned > | scc_succs |
Public Member Functions | |
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 |
Protected Member Functions | |
void | determine_usefulness () |
const scc_node & | node (unsigned scc) const |
Protected Attributes | |
std::vector< unsigned > | sccof_ |
std::vector< scc_node > | node_ |
const_twa_graph_ptr | aut_ |
Compute an SCC map and gather assorted information.
This takes twa_graph as input and compute its SCCs. This class maps all input states to their SCCs, and vice-versa. It allows iterating over all SCCs of the automaton, and check their acceptance or non-acceptance.
Additionally this class can be used on alternating automata, but in this case, universal transitions are handled like existential transitions. It still make sense to check which states belong to the same SCC, but the acceptance information computed by this class is meaningless.
|
inline |
Get number of the SCC containing the initial state.
std::vector<std::set<acc_cond::mark_t> > spot::scc_info::used_acc | ( | ) | const |
Return the set of all used acceptance combinations, for each accepting SCC.