A directed graph. More...

#include <spot/graph/graph.hh>

Inheritance diagram for spot::digraph< State_Data, Edge_Data >:

Collaboration diagram for spot::digraph< State_Data, Edge_Data >:

Public Types
enum	dump_storage_items { DSI_GraphHeader = 1 , DSI_GraphFooter = 2 , DSI_StatesHeader = 4 , DSI_StatesBody = 8 , DSI_StatesFooter = 16 , DSI_States = DSI_StatesHeader \| DSI_StatesBody \| DSI_StatesFooter , DSI_EdgesHeader = 32 , DSI_EdgesBody = 64 , DSI_EdgesFooter = 128 , DSI_Edges = DSI_EdgesHeader \| DSI_EdgesBody \| DSI_EdgesFooter , DSI_DestsHeader = 256 , DSI_DestsBody = 512 , DSI_DestsFooter = 1024 , DSI_Dests = DSI_DestsHeader \| DSI_DestsBody \| DSI_DestsFooter , DSI_All }
	Flags controlling dump_storage() output. More...

typedef internal::edge_iterator< digraph >	iterator
	Iterator over edges of a digraph.

typedef internal::edge_iterator< const digraph >	const_iterator
	Const iterator over edges of a digraph.

typedef State_Data	state_data_t
	State data type.

typedef Edge_Data	edge_data_t
	Edge data type.

typedef unsigned	state
	State number type.

typedef unsigned	edge
	Edge number type.

typedef internal::distate_storage< edge, internal::boxed_label< State_Data > >	state_storage_t
	State storage type.

typedef internal::edge_storage< state, state, edge, internal::boxed_label< Edge_Data > >	edge_storage_t
	Edge storage type.

typedef std::vector< state_storage_t >	state_vector
	Vector of state storage.

typedef std::vector< edge_storage_t >	edge_vector_t
	Vector of edge storage.

typedef std::vector< unsigned >	dests_vector_t
	Vector of universal destinations.

Public Member Functions
	digraph (unsigned max_states=10, unsigned max_trans=0)
	Construct an empty graph.

unsigned	num_states () const
	The number of states in the automaton.

unsigned	num_edges () const
	The number of edges in the automaton.

bool	is_existential () const
	Whether the automaton uses only existential branching.

template<typename... Args>
state	new_state (Args &&... args)
	Create a new state.

template<typename... Args>
state	new_states (unsigned n, Args &&... args)
	Create n new states.

template<typename... Args>
edge	new_edge (state src, state dst, Args &&... args)
	Create a new edge.

template<typename I >
state	new_univ_dests (I dst_begin, I dst_end)
	Create a new universal destination group.

template<typename I , typename... Args>
edge	new_univ_edge (state src, I dst_begin, I dst_end, Args &&... args)
	Create a new universal edge.

template<typename... Args>
edge	new_univ_edge (state src, const std::initializer_list< state > &dsts, Args &&... args)
	Create a new universal edge.

internal::const_universal_dests	univ_dests (state src) const
	Return universal destinations for state src.

internal::const_universal_dests	univ_dests (const edge_storage_t &e) const
	Return universal destinations for edge e.

state	index_of_state (const state_storage_t &ss) const
	Convert a storage reference into a state number.

edge	index_of_edge (const edge_storage_t &tt) const
	Convert a storage reference into an edge number.

bool	is_valid_edge (edge t) const
	Test whether the given edge is valid.

void	dump_storage (std::ostream &o) const
	Dump the state and edge storage for debugging.

void	dump_storage_as_dot (std::ostream &o, int dsi=DSI_All) const
	Dump the state and edge storage for debugging.

void	remove_dead_edges_ ()
	Remove all dead edges.

template<class Predicate = std::less<edge_storage_t>>
void	sort_edges_ (Predicate p=Predicate())
	Sort all edges according to a predicate.

template<class Predicate = std::less<edge_storage_t>>
void	sort_edges_srcfirst_ (Predicate p=Predicate(), parallel_policy ppolicy=parallel_policy())
	Sort all edges by src first, then, within edges of the same source, use the predicate.

template<bool Stable = false, class Predicate = std::less<edge_storage_t>>
void	sort_edges_of_ (Predicate p=Predicate(), const std::vector< bool > *to_sort_ptr=nullptr)
	Sort edges of the given states.

void	chain_edges_ ()
	Reconstruct the chain of outgoing edges.

void	rename_states_ (const std::vector< unsigned > &newst)
	Rename all the states in the edge vector.


state_storage_t &	state_storage (state s)
	Return a reference to the storage of a state.

const state_storage_t &	state_storage (state s) const
	Return a reference to the storage of a state.


state_storage_t::data_t &	state_data (state s)
	Return the State_Data associated to a state.

const state_storage_t::data_t &	state_data (state s) const
	Return the State_Data associated to a state.


edge_storage_t &	edge_storage (edge s)
	Return a reference to the storage of an edge.

const edge_storage_t &	edge_storage (edge s) const
	Return a reference to the storage of an edge.


edge_storage_t::data_t &	edge_data (edge s)
	Return the Edge_Data of an edge.

const edge_storage_t::data_t &	edge_data (edge s) const
	Return the Edge_Data of an edge.


internal::state_out< digraph >	out (state src)
	Return a fake container with all edges leaving src.

internal::state_out< digraph >	out (state_storage_t &src)
	Return a fake container with all edges leaving src.

internal::state_out< const digraph >	out (state src) const
	Return a fake container with all edges leaving src.

internal::state_out< const digraph >	out (state_storage_t &src) const
	Return a fake container with all edges leaving src.


internal::killer_edge_iterator< digraph >	out_iteraser (state_storage_t &src)
	Return a fake container with all edges leaving src, allowing erasure.

internal::killer_edge_iterator< digraph >	out_iteraser (state src)
	Return a fake container with all edges leaving src, allowing erasure.


const state_vector &	states () const
	Return the vector of states.

state_vector &	states ()
	Return the vector of states.


internal::all_trans< const digraph >	edges () const
	Return a fake container with all edges (excluding erased edges)

internal::all_trans< digraph >	edges ()
	Return a fake container with all edges (excluding erased edges)


const edge_vector_t &	edge_vector () const
	Return the vector of all edges.

edge_vector_t &	edge_vector ()
	Return the vector of all edges.


bool	is_dead_edge (unsigned t) const
	Test whether an edge has been erased.

bool	is_dead_edge (const edge_storage_t &t) const
	Test whether an edge has been erased.


const dests_vector_t &	dests_vector () const
	The vector used to store universal destinations.

dests_vector_t &	dests_vector ()
	The vector used to store universal destinations.


void	defrag_states (const std::vector< unsigned > &newst, unsigned used_states)
	Rename and remove states.

void	defrag_states (std::vector< unsigned > &&newst, unsigned used_states)
	Rename and remove states.

Protected Attributes
state_vector	states_
	State storage.

edge_vector_t	edges_
	Edge storage.

dests_vector_t	dests_
	Used by alternating automata.

unsigned	killed_edge_
	Number of erased edges.

Friends
class	internal::edge_iterator< digraph >

class	internal::edge_iterator< const digraph >

class	internal::killer_edge_iterator< digraph >

Detailed Description

template<typename State_Data, typename Edge_Data>
class spot::digraph< State_Data, Edge_Data >

A directed graph.

Template Parameters

State_Data	data to attach to states
Edge_Data	data to attach to edges

Member Typedef Documentation

◆ const_iterator

template<typename State_Data , typename Edge_Data >

typedef internal::edge_iterator<const digraph> spot::digraph< State_Data, Edge_Data >::const_iterator

Const iterator over edges of a digraph.

◆ dests_vector_t

template<typename State_Data , typename Edge_Data >

typedef std::vector<unsigned> spot::digraph< State_Data, Edge_Data >::dests_vector_t

Vector of universal destinations.

◆ edge

template<typename State_Data , typename Edge_Data >

typedef unsigned spot::digraph< State_Data, Edge_Data >::edge

Edge number type.

◆ edge_data_t

template<typename State_Data , typename Edge_Data >

typedef Edge_Data spot::digraph< State_Data, Edge_Data >::edge_data_t

Edge data type.

◆ edge_storage_t

template<typename State_Data , typename Edge_Data >

typedef internal::edge_storage<state, state, edge, internal::boxed_label<Edge_Data> > spot::digraph< State_Data, Edge_Data >::edge_storage_t

Edge storage type.

◆ edge_vector_t

template<typename State_Data , typename Edge_Data >

typedef std::vector<edge_storage_t> spot::digraph< State_Data, Edge_Data >::edge_vector_t

Vector of edge storage.

◆ iterator

template<typename State_Data , typename Edge_Data >

typedef internal::edge_iterator<digraph> spot::digraph< State_Data, Edge_Data >::iterator

Iterator over edges of a digraph.

◆ state

template<typename State_Data , typename Edge_Data >

typedef unsigned spot::digraph< State_Data, Edge_Data >::state

State number type.

◆ state_data_t

template<typename State_Data , typename Edge_Data >

typedef State_Data spot::digraph< State_Data, Edge_Data >::state_data_t

State data type.

◆ state_storage_t

template<typename State_Data , typename Edge_Data >

typedef internal::distate_storage<edge, internal::boxed_label<State_Data> > spot::digraph< State_Data, Edge_Data >::state_storage_t

State storage type.

◆ state_vector

template<typename State_Data , typename Edge_Data >

typedef std::vector<state_storage_t> spot::digraph< State_Data, Edge_Data >::state_vector

Vector of state storage.

Member Enumeration Documentation

◆ dump_storage_items

template<typename State_Data , typename Edge_Data >

enum spot::digraph::dump_storage_items

Flags controlling dump_storage() output.

Constructor & Destructor Documentation

◆ digraph()

template<typename State_Data , typename Edge_Data >

spot::digraph< State_Data, Edge_Data >::digraph	(	unsigned	max_states = `10`,
		unsigned	max_trans = `0`
	)

inline

Construct an empty graph.

Construct an empty graph, and reserve space for max_states states and max_trans edges. These are not hard limits, but just hints to pre-allocate a data structure that may hold that much items.

References spot::digraph< State_Data, Edge_Data >::edges_, and spot::digraph< State_Data, Edge_Data >::states_.

Member Function Documentation

◆ chain_edges_()

template<typename State_Data , typename Edge_Data >

void spot::digraph< State_Data, Edge_Data >::chain_edges_ ( )

inline

Reconstruct the chain of outgoing edges.

Should be called only when it is known that all edges with the same source are consecutive in the vector.

References spot::digraph< State_Data, Edge_Data >::edges_, and spot::digraph< State_Data, Edge_Data >::states_.

◆ defrag_states() [1/2]

template<typename State_Data , typename Edge_Data >

void spot::digraph< State_Data, Edge_Data >::defrag_states	(	const std::vector< unsigned > &	newst,
		unsigned	used_states
	)

inline

Rename and remove states.

This method is used to remove some states that have been previously detected to be unreachable in order to "defragment" the state vector. When a state is removed, all its outgoing transitions are removed as well. Removing reachable states should NOT be attempted, because the incoming edges will be dangling.

Parameters

newst	A vector indicating how each state should be renumbered. Use -1U to erase an unreachable state.
used_states	the number of states used (after renumbering)

References spot::digraph< State_Data, Edge_Data >::edges_, spot::digraph< State_Data, Edge_Data >::is_dead_edge(), spot::digraph< State_Data, Edge_Data >::killed_edge_, spot::permute_vector(), and spot::digraph< State_Data, Edge_Data >::states_.

Referenced by spot::digraph< State_Data, Edge_Data >::defrag_states().

◆ defrag_states() [2/2]

template<typename State_Data , typename Edge_Data >

void spot::digraph< State_Data, Edge_Data >::defrag_states	(	std::vector< unsigned > &&	newst,
		unsigned	used_states
	)

inline

Rename and remove states.

This method is used to remove some states that have been previously detected to be unreachable in order to "defragment" the state vector. When a state is removed, all its outgoing transitions are removed as well. Removing reachable states should NOT be attempted, because the incoming edges will be dangling.

Parameters

newst	A vector indicating how each state should be renumbered. Use -1U to erase an unreachable state.
used_states	the number of states used (after renumbering)

References spot::digraph< State_Data, Edge_Data >::defrag_states().

◆ dests_vector() [1/2]

template<typename State_Data , typename Edge_Data >

dests_vector_t & spot::digraph< State_Data, Edge_Data >::dests_vector ( )

inline

The vector used to store universal destinations.

The actual way those destinations are stored is an implementation detail you should not rely on.

References spot::digraph< State_Data, Edge_Data >::dests_.

◆ dests_vector() [2/2]

template<typename State_Data , typename Edge_Data >

const dests_vector_t & spot::digraph< State_Data, Edge_Data >::dests_vector ( ) const

inline

The vector used to store universal destinations.

The actual way those destinations are stored is an implementation detail you should not rely on.

References spot::digraph< State_Data, Edge_Data >::dests_.

Referenced by spot::twa_graph::operator==(), and spot::twa_graph::set_init_state().

◆ dump_storage()

template<typename State_Data , typename Edge_Data >

void spot::digraph< State_Data, Edge_Data >::dump_storage ( std::ostream & o ) const

inline

Dump the state and edge storage for debugging.

References spot::digraph< State_Data, Edge_Data >::dests_, spot::digraph< State_Data, Edge_Data >::edges_, and spot::digraph< State_Data, Edge_Data >::states_.

◆ dump_storage_as_dot()

template<typename State_Data , typename Edge_Data >

void spot::digraph< State_Data, Edge_Data >::dump_storage_as_dot	(	std::ostream &	o,
		int	dsi = `DSI_All`
	)		const

inline

Dump the state and edge storage for debugging.

References spot::digraph< State_Data, Edge_Data >::dests_, spot::digraph< State_Data, Edge_Data >::edges_, and spot::digraph< State_Data, Edge_Data >::states_.

◆ edge_data() [1/2]

template<typename State_Data , typename Edge_Data >

edge_storage_t::data_t & spot::digraph< State_Data, Edge_Data >::edge_data ( edge s )

inline

Return the Edge_Data of an edge.

This does not use Edge_Data& as return type, because Edge_Data might be void.

References spot::digraph< State_Data, Edge_Data >::edges_.

Referenced by spot::twa_graph::edge_data(), spot::twa_graph::edge_data(), spot::twa_graph::edge_data(), and spot::twa_graph::edge_data().

◆ edge_data() [2/2]

template<typename State_Data , typename Edge_Data >

const edge_storage_t::data_t & spot::digraph< State_Data, Edge_Data >::edge_data ( edge s ) const

inline

Return the Edge_Data of an edge.

This does not use Edge_Data& as return type, because Edge_Data might be void.

References spot::digraph< State_Data, Edge_Data >::edges_.

◆ edge_storage() [1/2]

template<typename State_Data , typename Edge_Data >

edge_storage_t & spot::digraph< State_Data, Edge_Data >::edge_storage ( edge s )

inline

Return a reference to the storage of an edge.

The storage includes any of the user-supplied Edge_Data, plus some custom fields needed to find the next transitions.

References spot::digraph< State_Data, Edge_Data >::edges_.

Referenced by spot::twa_graph::edge_storage(), spot::twa_graph::edge_storage(), spot::kripke_graph::edge_storage(), spot::twa_graph::edge_storage(), spot::kripke_graph::edge_storage(), and spot::twa_graph::edge_storage().

◆ edge_storage() [2/2]

template<typename State_Data , typename Edge_Data >

const edge_storage_t & spot::digraph< State_Data, Edge_Data >::edge_storage ( edge s ) const

inline

Return a reference to the storage of an edge.

The storage includes any of the user-supplied Edge_Data, plus some custom fields needed to find the next transitions.

References spot::digraph< State_Data, Edge_Data >::edges_.

◆ edge_vector() [1/2]

template<typename State_Data , typename Edge_Data >

edge_vector_t & spot::digraph< State_Data, Edge_Data >::edge_vector ( )

inline

Return the vector of all edges.

When using this method, beware that the first entry (edge #0) is not a real edge, and that any edge with next_succ pointing to itself is an erased edge.

You should probably use edges() instead.

References spot::digraph< State_Data, Edge_Data >::edges_.

◆ edge_vector() [2/2]

template<typename State_Data , typename Edge_Data >

const edge_vector_t & spot::digraph< State_Data, Edge_Data >::edge_vector ( ) const

inline

Return the vector of all edges.

When using this method, beware that the first entry (edge #0) is not a real edge, and that any edge with next_succ pointing to itself is an erased edge.

You should probably use edges() instead.

References spot::digraph< State_Data, Edge_Data >::edges_.

◆ edges() [1/2]

template<typename State_Data , typename Edge_Data >

internal::all_trans< digraph > spot::digraph< State_Data, Edge_Data >::edges ( )

inline

Return a fake container with all edges (excluding erased edges)

References spot::digraph< State_Data, Edge_Data >::edges_.

◆ edges() [2/2]

template<typename State_Data , typename Edge_Data >

internal::all_trans< const digraph > spot::digraph< State_Data, Edge_Data >::edges ( ) const

inline

Return a fake container with all edges (excluding erased edges)

References spot::digraph< State_Data, Edge_Data >::edges_.

Referenced by spot::kripke_graph::edges(), spot::twa_graph::edges(), spot::kripke_graph::edges(), and spot::twa_graph::edges().

◆ index_of_edge()

template<typename State_Data , typename Edge_Data >

edge spot::digraph< State_Data, Edge_Data >::index_of_edge ( const edge_storage_t & tt ) const

inline

Convert a storage reference into an edge number.

References spot::digraph< State_Data, Edge_Data >::edges_, and spot::tt.

Referenced by spot::twa_graph::edge_number(), and spot::digraph< State_Data, Edge_Data >::is_dead_edge().

◆ index_of_state()

template<typename State_Data , typename Edge_Data >

state spot::digraph< State_Data, Edge_Data >::index_of_state ( const state_storage_t & ss ) const

inline

Convert a storage reference into a state number.

References spot::digraph< State_Data, Edge_Data >::states_.

Referenced by spot::digraph< State_Data, Edge_Data >::out(), and spot::digraph< State_Data, Edge_Data >::out().

◆ is_dead_edge() [1/2]

template<typename State_Data , typename Edge_Data >

bool spot::digraph< State_Data, Edge_Data >::is_dead_edge ( const edge_storage_t & t ) const

inline

Test whether an edge has been erased.

See also: is_valid_edge

References spot::digraph< State_Data, Edge_Data >::index_of_edge().

◆ is_dead_edge() [2/2]

template<typename State_Data , typename Edge_Data >

bool spot::digraph< State_Data, Edge_Data >::is_dead_edge ( unsigned t ) const

inline

Test whether an edge has been erased.

See also: is_valid_edge

References spot::digraph< State_Data, Edge_Data >::edges_.

Referenced by spot::digraph< State_Data, Edge_Data >::defrag_states(), spot::twa_graph::is_dead_edge(), and spot::twa_graph::is_dead_edge().

◆ is_existential()

template<typename State_Data , typename Edge_Data >

bool spot::digraph< State_Data, Edge_Data >::is_existential ( ) const

inline

Whether the automaton uses only existential branching.

References spot::digraph< State_Data, Edge_Data >::dests_.

Referenced by spot::twa_graph::is_existential().

◆ is_valid_edge()

template<typename State_Data , typename Edge_Data >

bool spot::digraph< State_Data, Edge_Data >::is_valid_edge ( edge t ) const

inline

Test whether the given edge is valid.

An edge is valid if its number is less than the total number of edges, and it does not correspond to an erased (dead) edge.

See also: is_dead_edge()

References spot::digraph< State_Data, Edge_Data >::edges_.

Referenced by spot::kripke_graph::succ_iter(), and spot::twa_graph::succ_iter().

◆ new_edge()

template<typename State_Data , typename Edge_Data >

template<typename... Args>

edge spot::digraph< State_Data, Edge_Data >::new_edge	(	state	src,
		state	dst,
		Args &&...	args
	)

inline

Create a new edge.

Parameters

src	the source state
dst	the destination state
args	arguments to forward to the Edge_Data constructor

References spot::digraph< State_Data, Edge_Data >::edges_, and spot::digraph< State_Data, Edge_Data >::states_.

Referenced by spot::twa_graph::new_acc_edge(), spot::kripke_graph::new_edge(), and spot::digraph< State_Data, Edge_Data >::new_univ_edge().

◆ new_state()

template<typename State_Data , typename Edge_Data >

template<typename... Args>

state spot::digraph< State_Data, Edge_Data >::new_state ( Args &&... args )

inline

Create a new state.

All arguments are forwarded to the State_Data constructor.

Returns: a state number

References spot::digraph< State_Data, Edge_Data >::states_.

Referenced by spot::twa_graph::new_state(), and spot::kripke_graph::new_state().

◆ new_states()

template<typename State_Data , typename Edge_Data >

template<typename... Args>

state spot::digraph< State_Data, Edge_Data >::new_states	(	unsigned	n,
		Args &&...	args
	)

inline

Create n new states.

All arguments are forwarded to the State_Data constructor of each of the n states.

Returns: the first state number

References spot::digraph< State_Data, Edge_Data >::states_.

Referenced by spot::twa_graph::new_states(), and spot::kripke_graph::new_states().

◆ new_univ_dests()

template<typename State_Data , typename Edge_Data >

template<typename I >

state spot::digraph< State_Data, Edge_Data >::new_univ_dests	(	I	dst_begin,
		I	dst_end
	)

inline

Create a new universal destination group.

The resulting state number can be used as the destination of an edge.

Parameters

dst_begin	start of a non-empty container of destination states
dst_end	end of a non-empty container of destination states

References spot::digraph< State_Data, Edge_Data >::dests_.

Referenced by spot::digraph< State_Data, Edge_Data >::new_univ_edge(), and spot::twa_graph::set_univ_init_state().

◆ new_univ_edge() [1/2]

template<typename State_Data , typename Edge_Data >

template<typename... Args>

edge spot::digraph< State_Data, Edge_Data >::new_univ_edge	(	state	src,
		const std::initializer_list< state > &	dsts,
		Args &&...	args
	)

inline

Create a new universal edge.

Parameters

src	the source state
dsts	a non-empty list of destination states
args	arguments to forward to the Edge_Data constructor

References spot::digraph< State_Data, Edge_Data >::new_univ_edge().

◆ new_univ_edge() [2/2]

template<typename State_Data , typename Edge_Data >

template<typename I , typename... Args>

edge spot::digraph< State_Data, Edge_Data >::new_univ_edge	(	state	src,
		I	dst_begin,
		I	dst_end,
		Args &&...	args
	)

inline

Create a new universal edge.

Parameters

src	the source state
dst_begin	start of a non-empty container of destination states
dst_end	end of a non-empty container of destination states
args	arguments to forward to the Edge_Data constructor

References spot::digraph< State_Data, Edge_Data >::new_edge(), and spot::digraph< State_Data, Edge_Data >::new_univ_dests().

Referenced by spot::digraph< State_Data, Edge_Data >::new_univ_edge().

◆ num_edges()

template<typename State_Data , typename Edge_Data >

unsigned spot::digraph< State_Data, Edge_Data >::num_edges ( ) const

inline

The number of edges in the automaton.

Killed edges are omitted.

References spot::digraph< State_Data, Edge_Data >::edges_, and spot::digraph< State_Data, Edge_Data >::killed_edge_.

Referenced by spot::kripke_graph::num_edges(), and spot::twa_graph::num_edges().

◆ num_states()

template<typename State_Data , typename Edge_Data >

unsigned spot::digraph< State_Data, Edge_Data >::num_states ( ) const

inline

The number of states in the automaton.

References spot::digraph< State_Data, Edge_Data >::states_.

Referenced by spot::kripke_graph::num_states(), spot::twa_graph::num_states(), spot::digraph< State_Data, Edge_Data >::sort_edges_of_(), and spot::digraph< State_Data, Edge_Data >::sort_edges_srcfirst_().

◆ out() [1/4]

template<typename State_Data , typename Edge_Data >

internal::state_out< digraph > spot::digraph< State_Data, Edge_Data >::out ( state src )

inline

Return a fake container with all edges leaving src.

References spot::digraph< State_Data, Edge_Data >::states_.

Referenced by spot::digraph< State_Data, Edge_Data >::out(), spot::digraph< State_Data, Edge_Data >::out(), spot::kripke_graph::out(), spot::twa_graph::out(), spot::kripke_graph::out(), spot::twa_graph::out(), spot::digraph< State_Data, Edge_Data >::sort_edges_srcfirst_(), spot::twa_graph::state_acc_sets(), and spot::twa_graph::state_is_accepting().

◆ out() [2/4]

template<typename State_Data , typename Edge_Data >

internal::state_out< const digraph > spot::digraph< State_Data, Edge_Data >::out ( state src ) const

inline

Return a fake container with all edges leaving src.

References spot::digraph< State_Data, Edge_Data >::states_.

◆ out() [3/4]

template<typename State_Data , typename Edge_Data >

internal::state_out< digraph > spot::digraph< State_Data, Edge_Data >::out ( state_storage_t & src )

inline

Return a fake container with all edges leaving src.

References spot::digraph< State_Data, Edge_Data >::index_of_state(), and spot::digraph< State_Data, Edge_Data >::out().

◆ out() [4/4]

template<typename State_Data , typename Edge_Data >

internal::state_out< const digraph > spot::digraph< State_Data, Edge_Data >::out ( state_storage_t & src ) const

inline

Return a fake container with all edges leaving src.

References spot::digraph< State_Data, Edge_Data >::index_of_state(), and spot::digraph< State_Data, Edge_Data >::out().

◆ out_iteraser() [1/2]

template<typename State_Data , typename Edge_Data >

internal::killer_edge_iterator< digraph > spot::digraph< State_Data, Edge_Data >::out_iteraser ( state src )

inline

Return a fake container with all edges leaving src, allowing erasure.

References spot::digraph< State_Data, Edge_Data >::out_iteraser(), and spot::digraph< State_Data, Edge_Data >::state_storage().

◆ out_iteraser() [2/2]

template<typename State_Data , typename Edge_Data >

internal::killer_edge_iterator< digraph > spot::digraph< State_Data, Edge_Data >::out_iteraser ( state_storage_t & src )

inline

Return a fake container with all edges leaving src, allowing erasure.

Referenced by spot::digraph< State_Data, Edge_Data >::out_iteraser(), and spot::twa_graph::out_iteraser().

◆ remove_dead_edges_()

template<typename State_Data , typename Edge_Data >

void spot::digraph< State_Data, Edge_Data >::remove_dead_edges_ ( )

inline

Remove all dead edges.

The edges_ vector is left in a state that is incorrect and should eventually be fixed by a call to chain_edges_() before any iteration on the successor of a state is performed.

References spot::digraph< State_Data, Edge_Data >::edges_, and spot::digraph< State_Data, Edge_Data >::killed_edge_.

◆ rename_states_()

template<typename State_Data , typename Edge_Data >

void spot::digraph< State_Data, Edge_Data >::rename_states_ ( const std::vector< unsigned > & newst )

inline

Rename all the states in the edge vector.

The edges_ vector is left in a state that is incorrect and should eventually be fixed by a call to chain_edges_() before any iteration on the successor of a state is performed.

References spot::digraph< State_Data, Edge_Data >::edges_, and spot::digraph< State_Data, Edge_Data >::states_.

◆ sort_edges_()

template<typename State_Data , typename Edge_Data >

template<class Predicate = std::less<edge_storage_t>>

void spot::digraph< State_Data, Edge_Data >::sort_edges_ ( Predicate p = Predicate() )

inline

Sort all edges according to a predicate.

This will invalidate all iterators, and also destroy edge chains. Call chain_edges_() immediately afterwards unless you know what you are doing.

References spot::digraph< State_Data, Edge_Data >::edges_.

◆ sort_edges_of_()

template<typename State_Data , typename Edge_Data >

template<bool Stable = false, class Predicate = std::less<edge_storage_t>>

void spot::digraph< State_Data, Edge_Data >::sort_edges_of_	(	Predicate	p = `Predicate()`,
		const std::vector< bool > *	to_sort_ptr = `nullptr`
	)

inline

Sort edges of the given states.

Template Parameters

Predicate : Comparison type

Parameters

p	: Comparison callable
to_sort_ptr	: which states to sort. If null, all will be sorted

Note: No need to call chain_edges_, they are in a coherent state. todo: If pred does not involve bdd action other than id -> parallelize

References spot::digraph< State_Data, Edge_Data >::edges_, spot::digraph< State_Data, Edge_Data >::num_states(), and spot::digraph< State_Data, Edge_Data >::states_.

◆ sort_edges_srcfirst_()

template<typename State_Data , typename Edge_Data >

template<class Predicate = std::less<edge_storage_t>>

void spot::digraph< State_Data, Edge_Data >::sort_edges_srcfirst_	(	Predicate	p = `Predicate()`,
		parallel_policy	ppolicy = `parallel_policy()`
	)

inline

Sort all edges by src first, then, within edges of the same source, use the predicate.

This will invalidate all iterators, and also destroy edge chains. Call chain_edges_() immediately afterwards unless you know what you are doing.

Note: : for performance this will work in parallel (if enabled) and make a temporary copy of the edges (needs more ram)

Precondition: This needs the edge_vector to be in a coherent state when called

References spot::digraph< State_Data, Edge_Data >::edges_, spot::digraph< State_Data, Edge_Data >::num_states(), and spot::digraph< State_Data, Edge_Data >::out().

◆ state_data() [1/2]

template<typename State_Data , typename Edge_Data >

state_storage_t::data_t & spot::digraph< State_Data, Edge_Data >::state_data ( state s )

inline

Return the State_Data associated to a state.

This does not use State_Data& as return type, because State_Data might be void.

References spot::digraph< State_Data, Edge_Data >::states_.

Referenced by spot::kripke_graph::state_from_number(), spot::kripke_graph::state_from_number(), and spot::twa_graph::state_from_number().

◆ state_data() [2/2]

template<typename State_Data , typename Edge_Data >

const state_storage_t::data_t & spot::digraph< State_Data, Edge_Data >::state_data ( state s ) const

inline

Return the State_Data associated to a state.

This does not use State_Data& as return type, because State_Data might be void.

References spot::digraph< State_Data, Edge_Data >::states_.

◆ state_storage() [1/2]

template<typename State_Data , typename Edge_Data >

state_storage_t & spot::digraph< State_Data, Edge_Data >::state_storage ( state s )

inline

Return a reference to the storage of a state.

The storage includes any of the user-supplied State_Data, plus some custom fields needed to find the outgoing transitions.

References spot::digraph< State_Data, Edge_Data >::states_.

Referenced by spot::digraph< State_Data, Edge_Data >::out_iteraser(), spot::kripke_graph::state_number(), and spot::twa_graph::state_number().

◆ state_storage() [2/2]

template<typename State_Data , typename Edge_Data >

const state_storage_t & spot::digraph< State_Data, Edge_Data >::state_storage ( state s ) const

inline

Return a reference to the storage of a state.

The storage includes any of the user-supplied State_Data, plus some custom fields needed to find the outgoing transitions.

References spot::digraph< State_Data, Edge_Data >::states_.

◆ states() [1/2]

template<typename State_Data , typename Edge_Data >

state_vector & spot::digraph< State_Data, Edge_Data >::states ( )

inline

Return the vector of states.

References spot::digraph< State_Data, Edge_Data >::states_.

◆ states() [2/2]

template<typename State_Data , typename Edge_Data >

const state_vector & spot::digraph< State_Data, Edge_Data >::states ( ) const

inline

Return the vector of states.

References spot::digraph< State_Data, Edge_Data >::states_.

Referenced by spot::kripke_graph::states(), and spot::kripke_graph::states().

◆ univ_dests() [1/2]

template<typename State_Data , typename Edge_Data >

internal::const_universal_dests spot::digraph< State_Data, Edge_Data >::univ_dests ( const edge_storage_t & e ) const

inline

Return universal destinations for edge e.

References spot::digraph< State_Data, Edge_Data >::univ_dests().

◆ univ_dests() [2/2]

template<typename State_Data , typename Edge_Data >

internal::const_universal_dests spot::digraph< State_Data, Edge_Data >::univ_dests ( state src ) const

inline

Return universal destinations for state src.

References spot::digraph< State_Data, Edge_Data >::dests_.

Referenced by spot::digraph< State_Data, Edge_Data >::univ_dests(), spot::twa_graph::univ_dests(), and spot::twa_graph::univ_dests().

Member Data Documentation

◆ dests_

template<typename State_Data , typename Edge_Data >

dests_vector_t spot::digraph< State_Data, Edge_Data >::dests_

protected

Used by alternating automata.

Referenced by spot::digraph< State_Data, Edge_Data >::dests_vector(), spot::digraph< State_Data, Edge_Data >::dests_vector(), spot::digraph< State_Data, Edge_Data >::dump_storage(), spot::digraph< State_Data, Edge_Data >::dump_storage_as_dot(), spot::digraph< State_Data, Edge_Data >::is_existential(), spot::digraph< State_Data, Edge_Data >::new_univ_dests(), and spot::digraph< State_Data, Edge_Data >::univ_dests().

◆ edges_

template<typename State_Data , typename Edge_Data >

edge_vector_t spot::digraph< State_Data, Edge_Data >::edges_

protected

Edge storage.

◆ killed_edge_

template<typename State_Data , typename Edge_Data >

unsigned spot::digraph< State_Data, Edge_Data >::killed_edge_

protected

Number of erased edges.

Referenced by spot::digraph< State_Data, Edge_Data >::defrag_states(), spot::digraph< State_Data, Edge_Data >::num_edges(), and spot::digraph< State_Data, Edge_Data >::remove_dead_edges_().

◆ states_

template<typename State_Data , typename Edge_Data >

state_vector spot::digraph< State_Data, Edge_Data >::states_

protected

State storage.

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

spot/graph/graph.hh

Public Types

Public Member Functions

Protected Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ dests_vector_t

◆ edge

◆ edge_data_t

◆ edge_storage_t

◆ edge_vector_t

◆ iterator

◆ state

◆ state_data_t

◆ state_storage_t

◆ state_vector

Member Enumeration Documentation

◆ dump_storage_items

Constructor & Destructor Documentation

◆ digraph()

Member Function Documentation

◆ chain_edges_()

◆ defrag_states() [1/2]

◆ defrag_states() [2/2]

◆ dests_vector() [1/2]

◆ dests_vector() [2/2]

◆ dump_storage()

◆ dump_storage_as_dot()

◆ edge_data() [1/2]

◆ edge_data() [2/2]

◆ edge_storage() [1/2]

◆ edge_storage() [2/2]

◆ edge_vector() [1/2]

◆ edge_vector() [2/2]

◆ edges() [1/2]

◆ edges() [2/2]

◆ index_of_edge()

◆ index_of_state()

◆ is_dead_edge() [1/2]

◆ is_dead_edge() [2/2]

◆ is_existential()

◆ is_valid_edge()

◆ new_edge()

◆ new_state()

◆ new_states()

◆ new_univ_dests()

◆ new_univ_edge() [1/2]

◆ new_univ_edge() [2/2]

◆ num_edges()

◆ num_states()

◆ out() [1/4]

◆ out() [2/4]

◆ out() [3/4]

◆ out() [4/4]

◆ out_iteraser() [1/2]

◆ out_iteraser() [2/2]

◆ remove_dead_edges_()

◆ rename_states_()

◆ sort_edges_()

◆ sort_edges_of_()

◆ sort_edges_srcfirst_()

◆ state_data() [1/2]

◆ state_data() [2/2]

◆ state_storage() [1/2]

◆ state_storage() [2/2]

◆ states() [1/2]

◆ states() [2/2]

◆ univ_dests() [1/2]

◆ univ_dests() [2/2]

Member Data Documentation

◆ dests_

◆ edges_

◆ killed_edge_

◆ states_