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
	Alias for scc_info_node. More...

typedef scc_info_node::scc_succs	scc_succs
	Successor SCC list. More...

typedef spot::edge_filter_choice	edge_filter_choice
	Imported type. More...

typedef spot::edge_filter	edge_filter
	Imported edge filter type. More...

Public Member Functions
const_twa_graph_ptr	get_aut () const
	Return the automaton passed to the constructor. More...

scc_info_options	get_options () const
	Return the options used during construction. More...

edge_filter	get_filter () const
	Return the edge filter function. More...

void *	get_filter_data () const
	Return the user data passed to the edge filter. More...

unsigned	scc_count () const
	Return the total number of SCCs. More...

int	one_accepting_scc () const
	Return the number of one accepting SCC if any, -1 otherwise. More...

bool	reachable_state (unsigned st) const
	True if state st is reachable from the initial state. More...

unsigned	scc_of (unsigned st) const
	Return the SCC number containing state st. More...

std::vector< scc_node >::const_iterator	begin () const
	Iterator to the first SCC node. More...

std::vector< scc_node >::const_iterator	end () const
	Past-the-end iterator over SCC nodes. More...

std::vector< scc_node >::const_iterator	cbegin () const
	Const iterator to the first SCC node. More...

std::vector< scc_node >::const_iterator	cend () const
	Const past-the-end iterator over SCC nodes. More...

std::vector< scc_node >::const_reverse_iterator	rbegin () const
	Reverse iterator to the last SCC node. More...

std::vector< scc_node >::const_reverse_iterator	rend () const
	Reverse past-the-end iterator over SCC nodes. More...

const std::vector< unsigned > &	states_of (unsigned scc) const
	Return all states belonging to SCC scc. More...

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
	Return one arbitrary state in SCC scc. More...

unsigned	initial () const
	Get number of the SCC containing the initial state. More...

const scc_succs &	succ (unsigned scc) const
	Return the successor SCCs of SCC scc. More...

bool	is_trivial (unsigned scc) const
	True if SCC scc has no cycle. More...

bool	is_accepting_scc (unsigned scc) const
	True if SCC scc is necessarily accepting. More...

bool	is_rejecting_scc (unsigned scc) const
	True if SCC scc is necessarily rejecting. More...

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
	True if SCC scc can reach an accepting SCC. More...

bool	is_useful_state (unsigned st) const
	True if state st belongs to a useful SCC. More...

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
	Return the set of all marks appearing in SCC scc. More...

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
	Return a vector indicating which SCCs are weak. More...

bdd	scc_ap_support (unsigned scc) const
	Return the APs that appear in SCC scc. More...

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 ()
	Update the useful_ bits for all SCC nodes. More...

const scc_node &	node (unsigned scc) const
	Return the SCC node for the given SCC index. More...

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_
	SCC number for each state. More...

std::vector< scc_node >	node_
	SCC nodes in reverse topological order. More...

const_twa_graph_ptr	aut_
	The automaton being analyzed. More...

unsigned	initial_state_
	Initial state of the automaton. More...

edge_filter	filter_
	Optional edge filter function. More...

void *	filter_data_
	User data passed to the edge filter. More...

int	one_acc_scc_ = -1
	Index of one accepting SCC, or -1. More...

scc_info_options	options_
	Options used during construction. More...

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 spot::edge_filter spot::scc_info::edge_filter

Imported edge filter type.

◆ edge_filter_choice

typedef spot::edge_filter_choice spot::scc_info::edge_filter_choice

Imported type.

◆ scc_node

typedef scc_info_node spot::scc_info::scc_node

Alias for scc_info_node.

◆ scc_succs

typedef scc_info_node::scc_succs spot::scc_info::scc_succs

Successor SCC list.

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.

References spot::U.

◆ 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.

References spot::ALL.

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().

◆ begin()

std::vector<scc_node>::const_iterator spot::scc_info::begin ( ) const

inline

Iterator to the first SCC node.

◆ cbegin()

std::vector<scc_node>::const_iterator spot::scc_info::cbegin ( ) const

inline

Const iterator to the first SCC node.

◆ cend()

std::vector<scc_node>::const_iterator spot::scc_info::cend ( ) const

inline

Const past-the-end iterator over SCC nodes.

◆ check_scc_emptiness()

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().

◆ 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.

◆ determine_usefulness()

void spot::scc_info::determine_usefulness ( )

protected

Update the useful_ bits for all SCC nodes.

◆ 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.

◆ end()

std::vector<scc_node>::const_iterator spot::scc_info::end ( ) const

inline

Past-the-end iterator over SCC nodes.

◆ 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

scc	an accepting scc
r	a run to fill

This method needs the STOP_ON_ACC option.

◆ get_aut()

const_twa_graph_ptr spot::scc_info::get_aut ( ) const

inline

Return the automaton passed to the constructor.

◆ get_filter()

edge_filter spot::scc_info::get_filter ( ) const

inline

Return the edge filter function.

Referenced by spot::scc_and_mark_filter::scc_and_mark_filter().

◆ get_filter_data()

void* spot::scc_info::get_filter_data ( ) const

inline

Return the user data passed to the edge filter.

Referenced by spot::scc_and_mark_filter::scc_and_mark_filter().

◆ get_options()

scc_info_options spot::scc_info::get_options ( ) const

inline

Return the options used during construction.

◆ initial()

unsigned spot::scc_info::initial ( ) const

inline

Get number of the SCC containing the initial state.

◆ 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.

◆ is_accepting_scc()

bool spot::scc_info::is_accepting_scc ( unsigned scc ) const

inline

True if SCC scc is necessarily accepting.

◆ is_maximally_accepting_scc()

bool spot::scc_info::is_maximally_accepting_scc ( unsigned scc ) const

inline

Whether a cycle going through all edges of the SCC is accepting.

◆ is_rejecting_scc()

bool spot::scc_info::is_rejecting_scc ( unsigned scc ) const

inline

True if SCC scc is necessarily rejecting.

◆ is_trivial()

bool spot::scc_info::is_trivial ( unsigned scc ) const

inline

True if SCC scc has no cycle.

◆ is_useful_scc()

bool spot::scc_info::is_useful_scc ( unsigned scc ) const

inline

True if SCC scc can reach an accepting SCC.

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

◆ is_useful_state()

bool spot::scc_info::is_useful_state ( unsigned st ) const

inline

True if state st belongs to a useful 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.

◆ marks_of()

std::set<acc_cond::mark_t> spot::scc_info::marks_of ( unsigned scc ) const

Return the set of all marks appearing in SCC scc.

◆ node()

const scc_node& spot::scc_info::node ( unsigned scc ) const

inlineprotected

Return the SCC node for the given SCC index.

◆ one_accepting_scc()

int spot::scc_info::one_accepting_scc ( ) const

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.

◆ one_state_of()

unsigned spot::scc_info::one_state_of ( unsigned scc ) const

inline

Return one arbitrary state in SCC scc.

Referenced by spot::scc_and_mark_filter::start_state().

◆ rbegin()

std::vector<scc_node>::const_reverse_iterator spot::scc_info::rbegin ( ) const

inline

Reverse iterator to the last SCC node.

◆ reachable_state()

bool spot::scc_info::reachable_state ( unsigned st ) const

inline

True if state st is reachable from the initial state.

◆ rend()

std::vector<scc_node>::const_reverse_iterator spot::scc_info::rend ( ) const

inline

Reverse past-the-end iterator over SCC nodes.

◆ scc_ap_support()

bdd spot::scc_info::scc_ap_support ( unsigned scc ) const

Return the APs that appear in SCC scc.

◆ scc_count()

unsigned spot::scc_info::scc_count ( ) const

inline

Return the total number of SCCs.

◆ scc_of()

unsigned spot::scc_info::scc_of ( unsigned st ) const

inline

Return the SCC number containing state st.

◆ 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 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 [baier.19.atva] . 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.

See also: scc_and_mark_filter; generic_emptiness_check_for_scc

◆ states_of()

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

inline

Return all states belonging to SCC scc.

References spot::TRACK_STATES.

◆ 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().

◆ succ()

const scc_succs& spot::scc_info::succ ( unsigned scc ) const

inline

Return the successor SCCs of SCC scc.

References spot::TRACK_SUCCS.

◆ weak_sccs()

std::vector<bool> spot::scc_info::weak_sccs ( ) const

Return a vector indicating which SCCs are weak.

Member Data Documentation

◆ aut_

const_twa_graph_ptr spot::scc_info::aut_

protected

The automaton being analyzed.

◆ filter_

edge_filter spot::scc_info::filter_

protected

Optional edge filter function.

◆ filter_data_

void* spot::scc_info::filter_data_

protected

User data passed to the edge filter.

◆ initial_state_

unsigned spot::scc_info::initial_state_

protected

Initial state of the automaton.

◆ node_

std::vector<scc_node> spot::scc_info::node_

protected

SCC nodes in reverse topological order.

◆ one_acc_scc_

int spot::scc_info::one_acc_scc_ = -1

protected

Index of one accepting SCC, or -1.

◆ options_

scc_info_options spot::scc_info::options_

protected

Options used during construction.

◆ sccof_

std::vector<unsigned> spot::scc_info::sccof_

protected

SCC number for each state.

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

spot/twaalgos/sccinfo.hh

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ edge_filter

◆ edge_filter_choice

◆ scc_node

◆ scc_succs

Constructor & Destructor Documentation

◆ scc_info() [1/4]

◆ scc_info() [2/4]

◆ scc_info() [3/4]

◆ scc_info() [4/4]

Member Function Documentation

◆ acc_sets_of()

◆ begin()

◆ cbegin()

◆ cend()

◆ check_scc_emptiness()

◆ common_sets_of()

◆ determine_unknown_acceptance()

◆ determine_usefulness()

◆ edges_of()

◆ end()

◆ get_accepting_run()

◆ get_aut()

◆ get_filter()

◆ get_filter_data()

◆ get_options()

◆ initial()

◆ inner_edges_of()

◆ is_accepting_scc()

◆ is_maximally_accepting_scc()

◆ is_rejecting_scc()

◆ is_trivial()

◆ is_useful_scc()

◆ is_useful_state()

◆ marks()

◆ marks_of()

◆ node()

◆ one_accepting_scc()

◆ one_state_of()

◆ rbegin()

◆ reachable_state()

◆ rend()

◆ scc_ap_support()

◆ scc_count()

◆ scc_of()

◆ split_on_sets()

◆ states_of()

◆ states_on_acc_cycle_of()

◆ states_on_acc_cycle_of_rec()

◆ succ()

◆ weak_sccs()

Member Data Documentation

◆ aut_

◆ filter_

◆ filter_data_

◆ initial_state_

◆ node_

◆ one_acc_scc_

◆ options_

◆ sccof_