spot
2.4.3
|
Compute an SCC map and gather assorted information. More...
#include <spot/twaalgos/sccinfo.hh>
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 | |
scc_info (const_twa_graph_ptr aut, unsigned initial_state=~0U, edge_filter filter=nullptr, void *filter_data=nullptr) | |
const_twa_graph_ptr | get_aut () const |
unsigned | scc_count () const |
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_all > | edges_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_scc > | inner_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 () |
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 |
sets that contain at least one transition of the SCC More... | |
acc_cond::mark_t | common_sets_of (unsigned scc) const |
sets that contain the entire SCC More... | |
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_ |
unsigned | initial_state_ |
edge_filter | filter_ |
void * | filter_data_ |
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 make sense to check which states belong to the same SCC, but the acceptance information computed by this class is meaningless.
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()..
|
strong |
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()..
|
inline |
sets that contain at least one transition of the SCC
|
inline |
sets that contain the entire SCC
|
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.
|
inline |
Get number of the SCC containing the initial state.
|
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.
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.