spot  2.11.6
Public Types | Public Member Functions | Protected Attributes | Friends | List of all members
spot::digraph< State_Data, Edge_Data > Class Template Reference

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
}
 
typedef internal::edge_iterator< digraphiterator
 
typedef internal::edge_iterator< const digraphconst_iterator
 
typedef State_Data state_data_t
 
typedef Edge_Data edge_data_t
 
typedef unsigned state
 
typedef unsigned edge
 
typedef internal::distate_storage< edge, internal::boxed_label< State_Data > > state_storage_t
 
typedef internal::edge_storage< state, state, edge, internal::boxed_label< Edge_Data > > edge_storage_t
 
typedef std::vector< state_storage_tstate_vector
 
typedef std::vector< edge_storage_tedge_vector_t
 
typedef std::vector< unsigned > dests_vector_t
 

Public Member Functions

 digraph (unsigned max_states=10, unsigned max_trans=0)
 Construct an empty graph. More...
 
unsigned num_states () const
 The number of states in the automaton. More...
 
unsigned num_edges () const
 The number of edges in the automaton. More...
 
bool is_existential () const
 Whether the automaton uses only existential branching. More...
 
template<typename... Args>
state new_state (Args &&... args)
 Create a new states. More...
 
template<typename... Args>
state new_states (unsigned n, Args &&... args)
 Create n new states. More...
 
template<typename... Args>
edge new_edge (state src, state dst, Args &&... args)
 Create a new edge. More...
 
template<typename I >
state new_univ_dests (I dst_begin, I dst_end)
 Create a new universal destination group. More...
 
template<typename I , typename... Args>
edge new_univ_edge (state src, I dst_begin, I dst_end, Args &&... args)
 Create a new universal edge. More...
 
template<typename... Args>
edge new_univ_edge (state src, const std::initializer_list< state > &dsts, Args &&... args)
 Create a new universal edge. More...
 
internal::const_universal_dests univ_dests (state src) const
 
internal::const_universal_dests univ_dests (const edge_storage_t &e) const
 
state index_of_state (const state_storage_t &ss) const
 Convert a storage reference into a state number. More...
 
edge index_of_edge (const edge_storage_t &tt) const
 Convert a storage reference into an edge number. More...
 
bool is_valid_edge (edge t) const
 Test whether the given edge is valid. More...
 
void dump_storage (std::ostream &o) const
 Dump the state and edge storage for debugging. More...
 
void dump_storage_as_dot (std::ostream &o, int dsi=DSI_All) const
 Dump the state and edge storage for debugging. More...
 
void remove_dead_edges_ ()
 Remove all dead edges. More...
 
template<class Predicate = std::less<edge_storage_t>>
void sort_edges_ (Predicate p=Predicate())
 Sort all edges according to a predicate. More...
 
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. More...
 
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. More...
 
void chain_edges_ ()
 Reconstruct the chain of outgoing edges. More...
 
void rename_states_ (const std::vector< unsigned > &newst)
 Rename all the states in the edge vector. More...
 
state_storage_tstate_storage (state s)
 return a reference to the storage of a state More...
 
const state_storage_tstate_storage (state s) const
 return a reference to the storage of a state More...
 
state_storage_t::data_t & state_data (state s)
 return the State_Data associated to a state More...
 
const state_storage_t::data_t & state_data (state s) const
 return the State_Data associated to a state More...
 
edge_storage_tedge_storage (edge s)
 return a reference to the storage of an edge More...
 
const edge_storage_tedge_storage (edge s) const
 return a reference to the storage of an edge More...
 
edge_storage_t::data_t & edge_data (edge s)
 return the Edgeg_Data of an edge. More...
 
const edge_storage_t::data_t & edge_data (edge s) const
 return the Edgeg_Data of an edge. More...
 
internal::state_out< digraphout (state src)
 Return a fake container with all edges leaving src. More...
 
internal::state_out< digraphout (state_storage_t &src)
 Return a fake container with all edges leaving src. More...
 
internal::state_out< const digraphout (state src) const
 Return a fake container with all edges leaving src. More...
 
internal::state_out< const digraphout (state_storage_t &src) const
 Return a fake container with all edges leaving src. More...
 
internal::killer_edge_iterator< digraphout_iteraser (state_storage_t &src)
 Return a fake container with all edges leaving src, allowing erasure. More...
 
internal::killer_edge_iterator< digraphout_iteraser (state src)
 Return a fake container with all edges leaving src, allowing erasure. More...
 
const state_vector & states () const
 Return the vector of states. More...
 
state_vector & states ()
 Return the vector of states. More...
 
internal::all_trans< const digraphedges () const
 Return a fake container with all edges (exluding erased edges) More...
 
internal::all_trans< digraphedges ()
 Return a fake container with all edges (exluding erased edges) More...
 
const edge_vector_t & edge_vector () const
 Return the vector of all edges. More...
 
edge_vector_t & edge_vector ()
 Return the vector of all edges. More...
 
bool is_dead_edge (unsigned t) const
 Tests whether an edge has been erased. More...
 
bool is_dead_edge (const edge_storage_t &t) const
 Tests whether an edge has been erased. More...
 
const dests_vector_t & dests_vector () const
 The vector used to store universal destinations. More...
 
dests_vector_t & dests_vector ()
 The vector used to store universal destinations. More...
 
void defrag_states (const std::vector< unsigned > &newst, unsigned used_states)
 Rename and remove states. More...
 
void defrag_states (std::vector< unsigned > &&newst, unsigned used_states)
 Rename and remove states. More...
 

Protected Attributes

state_vector states_
 
edge_vector_t edges_
 
dests_vector_t dests_
 
unsigned killed_edge_
 

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_Datadata to attach to states
Edge_Datadata to attach to edges

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.

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.

◆ 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 transition are removed as well. Removing reachable states should NOT be attempted, because the incoming edges will be dangling.

Parameters
newstA vector indicating how each state should be renumbered. Use -1U to erase an unreachable state. All other numbers are expected to satisfy newst[i] ≤ i for all i.
used_statesthe number of states used (after renumbering)

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

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 transition are removed as well. Removing reachable states should NOT be attempted, because the incoming edges will be dangling.

Parameters
newstA vector indicating how each state should be renumbered. Use -1U to erase an unreachable state. All other numbers are expected to satisfy newst[i] ≤ i for all i.
used_statesthe 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.

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

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

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

◆ 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 Edgeg_Data of an edge.

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

◆ 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 Edgeg_Data of an edge.

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

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

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

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

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

◆ 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 (exluding erased 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 (exluding erased 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::tt.

Referenced by 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.

Referenced by 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

Tests 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

Tests whether an edge has been erased.

See also
is_valid_edge

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

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

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

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
srcthe source state
dstthe destination state
argsarguments to forward to the Edge_Data constructor

Referenced by 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 states.

All arguments are forwarded to the State_Data constructor.

Returns
a state number

◆ 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

◆ new_univ_dests()

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

Create a new universal destination group.

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

Parameters
dst_beginstart of a non-empty container of destination states
dst_endend of a non-empty container of destination states

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

◆ 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
srcthe source state
dstsa non-empty list of destination states
argsarguments 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,
dst_begin,
dst_end,
Args &&...  args 
)
inline

Create a new universal edge.

Parameters
srcthe source state
dst_beginstart of a non-empty container of destination states
dst_endend of a non-empty container of destination states
argsarguments 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.

◆ num_states()

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

◆ out() [1/4]

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

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

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

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

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

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

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

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

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

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

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

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

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


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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1