spot  2.3.5
Classes | Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
spot::scc_info Class Reference

Compute an SCC map and gather assorted information. More...

#include <spot/twaalgos/sccinfo.hh>

Collaboration diagram for spot::scc_info:
Collaboration graph

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_tused_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_nodenode (unsigned scc) const
 

Protected Attributes

std::vector< unsigned > sccof_
 
std::vector< scc_nodenode_
 
const_twa_graph_ptr aut_
 

Detailed Description

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.

Member Function Documentation

◆ initial()

unsigned spot::scc_info::initial ( ) const
inline

Get number of the SCC containing the initial state.

◆ used_acc()

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.


The documentation for this class was generated from the following file:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Thu Jun 22 2017 07:46:15 for spot by doxygen 1.8.13