A graph wrapper associating named states to graph state indices. More...

#include <spot/graph/ngraph.hh>

Collaboration diagram for spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >:

Public Types
typedef Graph::state	state
	State type. More...

typedef Graph::edge	edge
	Edge type. More...

typedef State_Name	name
	Name type. More...

typedef std::unordered_map< name, state, Name_Hash, Name_Equal >	name_to_state_t
	Map from name to state number type. More...

typedef std::vector< name >	state_to_name_t
	Map from state number to name type. More...

Public Member Functions
	named_graph (Graph &g)
	Construct wrapping graph g. More...

Graph &	graph ()
	Return the underlying graph. More...

Graph &	graph () const
	Return the underlying graph. More...

template<typename... Args>
state	new_state (name n, Args &&... args)
	Create a new state with the given name. More...

bool	alias_state (state s, name newname)
	Give an alternate name to a state. More...

state	get_state (name n) const
	Return the state number for the given name. More...

name	get_name (state s) const
	Return the name for the given state number. More...

bool	has_state (name n) const
	Return true iff a state with the given name exists. More...

const state_to_name_t &	names () const
	Return all state names. More...

template<typename... Args>
edge	new_edge (name src, name dst, Args &&... args)
	Add a new edge. More...

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

template<typename... Args>
edge	new_univ_edge (name src, const std::initializer_list< State_Name > &dsts, Args &&... args)
	Add a new universal edge. More...

Public Attributes
name_to_state_t	name_to_state

state_to_name_t	state_to_name
	Map from state number to name. More...

Protected Attributes
Graph &	g_
	The underlying graph. More...

Detailed Description

template<typename Graph, typename State_Name, typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>
class spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >

A graph wrapper associating named states to graph state indices.

Member Typedef Documentation

◆ edge

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

typedef Graph::edge spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::edge

Edge type.

◆ name

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

typedef State_Name spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::name

Name type.

◆ name_to_state_t

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

typedef std::unordered_map<name, state, Name_Hash, Name_Equal> spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::name_to_state_t

Map from name to state number type.

◆ state

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

typedef Graph::state spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::state

State type.

◆ state_to_name_t

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

typedef std::vector<name> spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::state_to_name_t

Map from state number to name type.

Constructor & Destructor Documentation

◆ named_graph()

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::named_graph ( Graph & g )

inline

Construct wrapping graph g.

Member Function Documentation

◆ get_name()

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

name spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::get_name ( state s ) const

inline

Return the name for the given state number.

◆ get_state()

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

state spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::get_state ( name n ) const

inline

Return the state number for the given name.

◆ graph() [1/2]

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

Graph& spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::graph ( )

inline

Return the underlying graph.

◆ graph() [2/2]

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

Graph& spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::graph ( ) const

inline

Return the underlying graph.

◆ has_state()

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

bool spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::has_state ( name n ) const

inline

Return true iff a state with the given name exists.

◆ names()

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

const state_to_name_t& spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::names ( ) const

inline

Return all state names.

◆ new_edge()

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

template<typename... Args>

edge spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::new_edge	(	name	src,
		name	dst,
		Args &&...	args
	)

inline

Add a new edge.

◆ new_state()

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

template<typename... Args>

state spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::new_state	(	name	n,
		Args &&...	args
	)

inline

Create a new state with the given name.

References spot::U.

◆ new_univ_edge() [1/2]

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

template<typename... Args>

edge spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::new_univ_edge	(	name	src,
		const std::initializer_list< State_Name > &	dsts,
		Args &&...	args
	)

inline

Add a new universal edge.

◆ new_univ_edge() [2/2]

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

template<typename I , typename... Args>

edge spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::new_univ_edge	(	name	src,
		I	dst_begin,
		I	dst_end,
		Args &&...	args
	)

inline

Add a new universal edge.

Member Data Documentation

◆ g_

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

Graph& spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::g_

protected

The underlying graph.

◆ name_to_state

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

name_to_state_t spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::name_to_state

Map from name to state number.

◆ state_to_name

template<typename Graph , typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

state_to_name_t spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >::state_to_name

Map from state number to name.

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

spot/graph/ngraph.hh

Public Types

Public Member Functions

Public Attributes

Protected Attributes

Detailed Description

template<typename Graph, typename State_Name, typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>> class spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >

Member Typedef Documentation

◆ edge

◆ name

◆ name_to_state_t

◆ state

◆ state_to_name_t

Constructor & Destructor Documentation

◆ named_graph()

Member Function Documentation

◆ get_name()

◆ get_state()

◆ graph() [1/2]

◆ graph() [2/2]

◆ has_state()

◆ names()

◆ new_edge()

◆ new_state()

◆ new_univ_edge() [1/2]

◆ new_univ_edge() [2/2]

Member Data Documentation

◆ g_

◆ name_to_state

◆ state_to_name

template<typename Graph, typename State_Name, typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>
class spot::named_graph< Graph, State_Name, Name_Hash, Name_Equal >