|
spot 2.12.2
|
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 |
| typedef spot::edge_filter_choice | edge_filter_choice |
| typedef spot::edge_filter | edge_filter |
Public Member Functions | |
| const_twa_graph_ptr | get_aut () const |
| scc_info_options | get_options () const |
| edge_filter | get_filter () 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_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 |
| bool | is_maximally_accepting_scc (unsigned scc) const |
| Whether a cycle going through all edges of the SCC is accepting. More... | |
| 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) const |
| 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_t > | marks_of (unsigned scc) const |
| std::vector< std::set< acc_cond::mark_t > > | used_acc () const |
| std::set< acc_cond::mark_t > | used_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_node & | node (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_node > | node_ |
| const_twa_graph_ptr | aut_ |
| unsigned | initial_state_ |
| edge_filter | filter_ |
| void * | filter_data_ |
| int | one_acc_scc_ = -1 |
| scc_info_options | options_ |
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.
| 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.
|
inline |
| 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.
|
inline |
|
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().
| bool spot::scc_info::check_scc_emptiness | ( | unsigned | n | ) | const |
Recompute whether an SCC is accepting or not.
This is an internal function of determine_unknown_acceptance().
|
inline |
Returns, for a given SCC, the set of colors that appear on all of its transitions.
| 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.
|
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.
| 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.
| scc | an accepting scc |
| r | a run to fill |
This method needs the STOP_ON_ACC option.
|
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.
|
inline |
Whether a cycle going through all edges of the SCC is accepting.
| 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.
|
inline |
Return the number of one accepting SCC if any, -1 otherwise.
If an accepting SCC has been found, return its number. Otherwise return -1. Note that when the acceptance condition contains Fin, -1 does not imply that all SCCs are rejecting: it just means that no accepting SCC is known currently. In that case, you might want to call determine_unknown_acceptance() first.
| 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 with disjoint sets of transitions that cover all cycles that remain after the removal. Two cycles that share a state are guaranteed to be in the same automaton. State and transitions that do not belong to any cycle after removal may or may not be covered by the returned automata. All returned automata have at least one edge, but it is also possible that they may not contain any cycle.
Set preserve_names to True if you want to keep the original name of each states for display. (This is a bit slower.)
This method was originally used as a part of our generic emptiness check [2] . However, creating new automata made it quite slow, so today our generic emptiness check does not use split_on_sets(). Instead, it passes an scc_and_mark_filter to scc_info in order to explore SCCs while ignoring edges with some given colors and without any copy.
| 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.
|
protected |
: Recursive function used by states_on_acc_cycle_of().
1.9.4