spot  2.8.3
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members

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

#include <spot/twaalgos/sccinfo.hh>

Collaboration diagram for spot::scc_info:

Public Types

typedef scc_info_node scc_node
 
typedef scc_info_node::scc_succs scc_succs
 
enum  edge_filter_choice { keep, ignore, cut }
 An edge_filter may be called on each edge to decide what to do with it. More...
 
typedef edge_filter_choice(* edge_filter) (const twa_graph::edge_storage_t &e, unsigned dst, void *filter_data)
 An edge_filter may be called on each edge to decide what to do with it. More...
 

Public Member Functions

const_twa_graph_ptr get_aut () const
 
scc_info_options get_options () const
 
const void * get_filter_data () const
 
unsigned scc_count () const
 
int one_accepting_scc () const
 Return the number of one accepting SCC if any, -1 otherwise. More...
 
bool reachable_state (unsigned st) const
 
unsigned scc_of (unsigned st) const
 
std::vector< scc_node >::const_iterator begin () const
 
std::vector< scc_node >::const_iterator end () const
 
std::vector< scc_node >::const_iterator cbegin () const
 
std::vector< scc_node >::const_iterator cend () const
 
std::vector< scc_node >::const_reverse_iterator rbegin () const
 
std::vector< scc_node >::const_reverse_iterator rend () const
 
const std::vector< unsigned > & states_of (unsigned scc) const
 
internal::scc_edges< const twa_graph::graph_t, internal::keep_alledges_of (unsigned scc) const
 A fake container to iterate over all edges leaving any state of an SCC. More...
 
internal::scc_edges< const twa_graph::graph_t, internal::keep_inner_sccinner_edges_of (unsigned scc) const
 A fake container to iterate over all edges between states of an SCC. More...
 
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 ()
 Study the SCCs that are currently reported neither as accepting nor as rejecting because of the presence of Fin sets. More...
 
bool check_scc_emptiness (unsigned n)
 Recompute whether an SCC is accepting or not. More...
 
void get_accepting_run (unsigned scc, twa_run_ptr r) const
 Retrieves an accepting run of the automaton whose cycle is in the SCC. More...
 
bool is_useful_scc (unsigned scc) const
 
bool is_useful_state (unsigned st) const
 
std::vector< std::set< acc_cond::mark_t > > marks () const
 Returns, for each accepting SCC, the set of all marks appearing in it. More...
 
std::set< acc_cond::mark_tmarks_of (unsigned scc) const
 
std::vector< std::set< acc_cond::mark_t > > used_acc () const
 
std::set< acc_cond::mark_tused_acc_of (unsigned scc) const
 
acc_cond::mark_t acc_sets_of (unsigned scc) const
 Returns, for a given SCC, the set of all colors appearing in it. It is the set of colors that appear in some mark among those returned by marks_of(). More...
 
acc_cond::mark_t common_sets_of (unsigned scc) const
 
std::vector< bool > weak_sccs () const
 
bdd scc_ap_support (unsigned scc) const
 
std::vector< twa_graph_ptr > split_on_sets (unsigned scc, acc_cond::mark_t sets, bool preserve_names=false) const
 Split an SCC into multiple automata separated by some acceptance sets. More...
 
std::vector< unsigned > states_on_acc_cycle_of (unsigned scc) const
 : Get all states visited by any accepting cycles of the 'scc'. More...
 
 scc_info (const_twa_graph_ptr aut, unsigned initial_state=~0U, edge_filter filter=nullptr, void *filter_data=nullptr, scc_info_options options=scc_info_options::ALL)
 Create the scc_info map for aut. More...
 
 scc_info (const_twa_graph_ptr aut, scc_info_options options)
 Create the scc_info map for aut. More...
 
 scc_info (const scc_and_mark_filter &filt, scc_info_options options)
 Create an scc_info map from some filter. More...
 
 scc_info (const scc_and_mark_filter &filt)
 Create an scc_info map from some filter. More...
 

Protected Member Functions

void determine_usefulness ()
 
const scc_nodenode (unsigned scc) const
 
void states_on_acc_cycle_of_rec (unsigned scc, acc_cond::mark_t all_fin, acc_cond::mark_t all_inf, unsigned nb_pairs, std::vector< acc_cond::rs_pair > &pairs, std::vector< unsigned > &res, std::vector< unsigned > &old) const
 : Recursive function used by states_on_acc_cycle_of(). More...
 

Protected Attributes

std::vector< unsigned > sccof_
 
std::vector< scc_nodenode_
 
const_twa_graph_ptr aut_
 
unsigned initial_state_
 
edge_filter filter_
 
void * filter_data_
 
int one_acc_scc_ = -1
 
scc_info_options options_
 

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 checks their acceptance or non-acceptance.

SCC are numbered in reverse topological order, i.e. the SCC of the initial state has the highest number, and if s1 is reachable from s2, then s1 < s2. Many algorithms depend on this property to determine in what order to iterate the SCCs.

Additionally this class can be used on alternating automata, but in this case, universal transitions are handled like existential transitions. It still makes sense to check which states belong to the same SCC, but the acceptance information computed by this class is meaningless.

Member Typedef Documentation

◆ edge_filter

typedef edge_filter_choice(* spot::scc_info::edge_filter) (const twa_graph::edge_storage_t &e, unsigned dst, void *filter_data)

An edge_filter may be called on each edge to decide what to do with it.

The edge filter is called with an edge and a destination. (In existential automata the destination is already given by the edge, but in alternating automata, one edge may have several destinations, and in this case the filter will be called for each destination.) The filter should return a value from edge_filter_choice.

keep means to use the edge normally, as if no filter had been given. ignore means to pretend the edge does not exist (if the destination is only reachable through this edge, it will not be visited). cut also ignores the edge, but it remembers to visit the destination state (as if it were an initial state) in case it is not reachable otherwise.

Note that successors between SCCs can only be maintained for edges that are kept. If some edges are ignored or cut, the SCC graph that you can explore with scc_info::initial() and scc_info::succ() will be restricted to the portion reachable with "keep" edges. Additionally SCCs might be created when edges are cut, but those will not be reachable from scc_info::initial()..

Member Enumeration Documentation

◆ edge_filter_choice

An edge_filter may be called on each edge to decide what to do with it.

The edge filter is called with an edge and a destination. (In existential automata the destination is already given by the edge, but in alternating automata, one edge may have several destinations, and in this case the filter will be called for each destination.) The filter should return a value from edge_filter_choice.

keep means to use the edge normally, as if no filter had been given. ignore means to pretend the edge does not exist (if the destination is only reachable through this edge, it will not be visited). cut also ignores the edge, but it remembers to visit the destination state (as if it were an initial state) in case it is not reachable otherwise.

Note that successors between SCCs can only be maintained for edges that are kept. If some edges are ignored or cut, the SCC graph that you can explore with scc_info::initial() and scc_info::succ() will be restricted to the portion reachable with "keep" edges. Additionally SCCs might be created when edges are cut, but those will not be reachable from scc_info::initial()..

Constructor & Destructor Documentation

◆ scc_info() [1/4]

spot::scc_info::scc_info ( const_twa_graph_ptr  aut,
unsigned  initial_state = ~0U,
edge_filter  filter = nullptr,
void *  filter_data = nullptr,
scc_info_options  options = scc_info_options::ALL 
)

Create the scc_info map for aut.

◆ scc_info() [2/4]

spot::scc_info::scc_info ( const_twa_graph_ptr  aut,
scc_info_options  options 
)
inline

Create the scc_info map for aut.

◆ scc_info() [3/4]

spot::scc_info::scc_info ( const scc_and_mark_filter filt,
scc_info_options  options 
)

Create an scc_info map from some filter.

This is usually used to prevent some edges from being considered as part of cycles, and can additionally restrict to exploration to some SCC discovered by another SCC.

◆ scc_info() [4/4]

spot::scc_info::scc_info ( const scc_and_mark_filter filt)
inline

Create an scc_info map from some filter.

This is usually used to prevent some edges from being considered as part of cycles, and can additionally restrict to exploration to some SCC discovered by another SCC.

Member Function Documentation

◆ acc_sets_of()

acc_cond::mark_t spot::scc_info::acc_sets_of ( unsigned  scc) const
inline

Returns, for a given SCC, the set of all colors appearing in it. It is the set of colors that appear in some mark among those returned by marks_of().

◆ check_scc_emptiness()

bool spot::scc_info::check_scc_emptiness ( unsigned  n)

Recompute whether an SCC is accepting or not.

This is an internal function of determine_unknown_acceptance().

◆ common_sets_of()

acc_cond::mark_t spot::scc_info::common_sets_of ( unsigned  scc) const
inline

Returns, for a given SCC, the set of colors that appear on all of its transitions.

◆ determine_unknown_acceptance()

void spot::scc_info::determine_unknown_acceptance ( )

Study the SCCs that are currently reported neither as accepting nor as rejecting because of the presence of Fin sets.

This simply calls check_scc_emptiness() on undeterminate SCCs.

◆ edges_of()

internal::scc_edges<const twa_graph::graph_t, internal::keep_all> spot::scc_info::edges_of ( unsigned  scc) const
inline

A fake container to iterate over all edges leaving any state of an SCC.

The difference with inner_edges_of() is that edges_of() include outgoing edges from all the states, even if they leave the SCC.

◆ get_accepting_run()

void spot::scc_info::get_accepting_run ( unsigned  scc,
twa_run_ptr  r 
) const

Retrieves an accepting run of the automaton whose cycle is in the SCC.

Parameters
sccan accepting scc
ra run to fill

This method needs the STOP_ON_ACC option.

◆ initial()

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

Get number of the SCC containing the initial state.

References spot::STOP_ON_ACC, and spot::TRACK_SUCCS.

◆ inner_edges_of()

internal::scc_edges<const twa_graph::graph_t, internal::keep_inner_scc> spot::scc_info::inner_edges_of ( unsigned  scc) const
inline

A fake container to iterate over all edges between states of an SCC.

The difference with edges_of() is that inner_edges_of() ignores edges leaving the SCC. In the case of an alternating automaton, an edge is considered to be part of the SCC of one of its destination is in the SCC.

◆ marks()

std::vector<std::set<acc_cond::mark_t> > spot::scc_info::marks ( ) const

Returns, for each accepting SCC, the set of all marks appearing in it.

◆ one_accepting_scc()

int spot::scc_info::one_accepting_scc ( ) const
inline

Return the number of one accepting SCC if any, -1 otherwise.

References spot::TRACK_STATES, and spot::U.

◆ split_on_sets()

std::vector<twa_graph_ptr> spot::scc_info::split_on_sets ( unsigned  scc,
acc_cond::mark_t  sets,
bool  preserve_names = false 
) const

Split an SCC into multiple automata separated by some acceptance sets.

Pretend that the transitions of SCC scc that belong to any of the sets given in sets have been removed, and return a set of automata necessary to cover all remaining states.

Set preserve_names to True if you want to keep the original name of each states for display. (This is a bit slower.)

◆ states_on_acc_cycle_of()

std::vector<unsigned> spot::scc_info::states_on_acc_cycle_of ( unsigned  scc) const

: Get all states visited by any accepting cycles of the 'scc'.

Throws an exception if the automaton does not have a 'Streett-like' acceptance condition.

◆ states_on_acc_cycle_of_rec()

void spot::scc_info::states_on_acc_cycle_of_rec ( unsigned  scc,
acc_cond::mark_t  all_fin,
acc_cond::mark_t  all_inf,
unsigned  nb_pairs,
std::vector< acc_cond::rs_pair > &  pairs,
std::vector< unsigned > &  res,
std::vector< unsigned > &  old 
) const
protected

: Recursive function used by states_on_acc_cycle_of().


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 Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13