#include <Graph.h>

Public Types
enum class	EdgeDirection { EDGE_NONE = 0 , EDGE_SUCCESSOR = 1 , EDGE_PREDECESSOR = 2 , EDGE_BIDIRECTIONAL = 3 }

using	const_iterator = const verti *

using	edge_list = std::vector< std::pair< verti, verti > >

Public Member Functions
	StaticGraph ()

	~StaticGraph ()

void	clear ()

void	make_random (verti V, unsigned outdeg, EdgeDirection edge_dir, bool scc)

void	make_random_clustered (verti cluster_size, verti V, unsigned outdeg, EdgeDirection edge_dir)

void	shuffle_vertices ()

void	shuffle_vertices (const std::vector< verti > &perm)

void	assign (const StaticGraph &graph)

void	assign (edge_list edges, EdgeDirection edge_dir)

edge_list	get_edges () const

template<class ForwardIterator >
void	make_subgraph (const StaticGraph &graph, ForwardIterator vertices_begin, ForwardIterator vertices_end, bool proper, EdgeDirection edge_dir=EdgeDirection::EDGE_NONE)

void	make_subgraph_threads (const StaticGraph &graph, const verti *verts, verti nvert, bool proper, EdgeDirection edge_dir=EdgeDirection::EDGE_NONE)

void	remove_edges (edge_list &edges)

void	write_raw (std::ostream &os) const

void	read_raw (std::istream &is)

void	swap (StaticGraph &g) noexcept

bool	empty () const

verti	V () const

edgei	E () const

EdgeDirection	edge_dir () const

const_iterator	succ_begin (verti v) const

const_iterator	succ_end (verti v) const

const_iterator	pred_begin (verti v) const

const_iterator	pred_end (verti v) const

bool	has_succ (verti v, verti w) const

bool	has_pred (verti w, verti v) const

edgei	degree (verti v) const

edgei	outdegree (verti v) const

edgei	indegree (verti v) const

	StaticGraph (const StaticGraph &graph)=delete

StaticGraph &	operator= (const StaticGraph &graph)=delete

Protected Member Functions
void	make_random_scc (edge_list &edges)

void	reset (verti V, edgei E, EdgeDirection edge_dir)

template<class ForwardIterator , class VertexMapT >
void	make_subgraph (const StaticGraph &graph, ForwardIterator vertices_begin, ForwardIterator vertices_end, VertexMapT &vertex_map, bool proper, EdgeDirection edge_dir=EdgeDirection::EDGE_NONE)

Private Attributes
verti	V_ = 0UL

edgei	E_ = 0UL

verti *	successors_ = nullptr

verti *	predecessors_ = nullptr

edgei *	successor_index_ = nullptr

edgei *	predecessor_index_ = nullptr

EdgeDirection	edge_dir_

Friends
class	SmallProgressMeasures

class	EdgeIterator

constexpr bool	operator& (EdgeDirection a, EdgeDirection b)

Detailed Description

A static graph consists of V vertices (numbered from 0 to V, exclusive) and E edges, and can store either edge successors, predecessors, or both.

Definition at line 35 of file Graph.h.

Member Typedef Documentation

◆ const_iterator

using StaticGraph::const_iterator = const verti*

Iterator used to iterate over predecessor/successor vertices.

Definition at line 66 of file Graph.h.

◆ edge_list

using StaticGraph::edge_list = std::vector<std::pair<verti, verti> >

A list of edges

Definition at line 74 of file Graph.h.

Member Enumeration Documentation

◆ EdgeDirection

enum class StaticGraph::EdgeDirection

strong

Specifies which parts of the edges are stored. When storing successors only, the functions succ_begin() and succ_end() can be used to iterate over the successors of a given vertex. Conversely, when storing predecessors, pred_begin() and pred_end() can be used to iterate over predecessors. When storing bidirectional edges, both pairs of functions can be used, but this requires more memory.

Enumerator
EDGE_NONE
EDGE_SUCCESSOR
EDGE_PREDECESSOR
EDGE_BIDIRECTIONAL

Definition at line 83 of file Graph.h.

Constructor & Destructor Documentation

◆ StaticGraph() [1/2]

StaticGraph::StaticGraph ( )

Construct an empty static graph.

Definition at line 16 of file Graph.cpp.

◆ ~StaticGraph()

StaticGraph::~StaticGraph ( )

Destroy the static graph.

Definition at line 21 of file Graph.cpp.

◆ StaticGraph() [2/2]

StaticGraph::StaticGraph ( const StaticGraph & graph )

explicitdelete

Member Function Documentation

◆ assign() [1/2]

void StaticGraph::assign ( const StaticGraph & graph )

Reset the graph to a copy of graph.

Definition at line 302 of file Graph.cpp.

◆ assign() [2/2]

void StaticGraph::assign	(	edge_list	edges,
		EdgeDirection	edge_dir
	)

Reset the graph based on the given edge structure.

Definition at line 325 of file Graph.cpp.

◆ clear()

void StaticGraph::clear ( )

Reset to an empty graph.

Definition at line 29 of file Graph.cpp.

◆ degree()

edgei StaticGraph::degree ( verti v ) const

inline

Returns the degree for vertex v.

Definition at line 226 of file Graph.h.

◆ E()

edgei StaticGraph::E ( ) const

inline

Returns the number of edges in the graph.

Definition at line 190 of file Graph.h.

◆ edge_dir()

EdgeDirection StaticGraph::edge_dir ( ) const

inline

Return direction of edges stored.

Definition at line 193 of file Graph.h.

◆ empty()

bool StaticGraph::empty ( ) const

inline

Returns whether the graph is empty.

Definition at line 184 of file Graph.h.

◆ get_edges()

StaticGraph::edge_list StaticGraph::get_edges ( ) const

Convert the graph into a list of edges.

Definition at line 493 of file Graph.cpp.

◆ has_pred()

bool StaticGraph::has_pred	(	verti	w,
		verti	v
	)		const

inline

Returns whether w has a predecessor v.

Definition at line 221 of file Graph.h.

◆ has_succ()

bool StaticGraph::has_succ	(	verti	v,
		verti	w
	)		const

inline

Returns whether v has a successor w.

Definition at line 216 of file Graph.h.

◆ indegree()

edgei StaticGraph::indegree ( verti v ) const

inline

Returns the indegree for vertex v.

Definition at line 236 of file Graph.h.

◆ make_random()

void StaticGraph::make_random	(	verti	V,
		unsigned	outdeg,
		EdgeDirection	edge_dir,
		bool	scc
	)

Generate a random graph (replacing the old contents). The resulting game does not contain loops.

Parameters

V	number of vertices to generate
outdeg	desired average outdegree (at least 1)
edge_dir	which parts of edges to store
scc	create a single strongly-connected component

Definition at line 146 of file Graph.cpp.

◆ make_random_clustered()

void StaticGraph::make_random_clustered	(	verti	cluster_size,
		verti	V,
		unsigned	outdeg,
		EdgeDirection	edge_dir
	)

Generate a random clustered game, which is based on random games of size cluster_size each, which are connected recursively by being substituting for the vertices of another game of size cluster_size, repeatedly, until a single game remains.

The resulting game is always a single connected component without loops.

Passing V <= cluster_size is equivalent to calling make_random() with scc = true. Choosing V = cluster_size^d creates a game with recursion depth d.

Parameters

cluster_size	number of vertices per cluster
V	total number of vertices to generate
outdeg	average outdegree (at least 1)
edge_dir	which parts of the edges to store

See also: make_random

Definition at line 205 of file Graph.cpp.

◆ make_random_scc()

void StaticGraph::make_random_scc ( edge_list & edges )

protected

Turn the current graph (with current edge list passed in edges) into a strongly connected component by randomly adding edges where necessary.

Definition at line 88 of file Graph.cpp.

◆ make_subgraph() [1/2]

template<class ForwardIterator >

void StaticGraph::make_subgraph	(	const StaticGraph &	graph,
		ForwardIterator	vertices_begin,
		ForwardIterator	vertices_end,
		bool	proper,
		StaticGraph::EdgeDirection	edge_dir = `EdgeDirection::EDGE_NONE`
	)

Reset the graph to the subgraph induced by the given vertex set.

Definition at line 52 of file Graph_impl.h.

◆ make_subgraph() [2/2]

template<class ForwardIterator , class VertexMapT >

void StaticGraph::make_subgraph	(	const StaticGraph &	graph,
		ForwardIterator	vertices_begin,
		ForwardIterator	vertices_end,
		VertexMapT &	vertex_map,
		bool	proper,
		EdgeDirection	edge_dir = `EdgeDirection::EDGE_NONE`
	)

protected

Reset the graph to the subgraph induced by the given vertex set, using the given map data structure to create the vertex mapping.

Definition at line 76 of file Graph_impl.h.

◆ make_subgraph_threads()

void StaticGraph::make_subgraph_threads	(	const StaticGraph &	graph,
		const verti *	verts,
		verti	nvert,
		bool	proper,
		EdgeDirection	edge_dir = `EdgeDirection::EDGE_NONE`
	)

◆ operator=()

StaticGraph & StaticGraph::operator= ( const StaticGraph & graph )

delete

◆ outdegree()

edgei StaticGraph::outdegree ( verti v ) const

inline

Returns the outdegree for vertex v.

Definition at line 231 of file Graph.h.

◆ pred_begin()

const_iterator StaticGraph::pred_begin ( verti v ) const

inline

Returns an iterator pointing to the first predecessor of vertex v.

Definition at line 206 of file Graph.h.

◆ pred_end()

const_iterator StaticGraph::pred_end ( verti v ) const

inline

Returns an iterator pointing past the last predecessor of vertex v.

Definition at line 211 of file Graph.h.

◆ read_raw()

void StaticGraph::read_raw ( std::istream & is )

Read raw graph data from input stream

Definition at line 530 of file Graph.cpp.

◆ remove_edges()

void StaticGraph::remove_edges ( StaticGraph::edge_list & edges )

Removes the given edges from the graph. The contents of the edge list may be reordered by this function!

Definition at line 400 of file Graph.cpp.

◆ reset()

void StaticGraph::reset	(	verti	V,
		edgei	E,
		EdgeDirection	edge_dir
	)

protected

Frees allocated memory and then reallocates memory to store a graph with V vertices and E edges.

Definition at line 34 of file Graph.cpp.

◆ shuffle_vertices() [1/2]

void StaticGraph::shuffle_vertices ( )

Randomly shuffles vertex indices. This is useful to obfuscate some of the structure remaining after make_random_clustered().

Definition at line 280 of file Graph.cpp.

◆ shuffle_vertices() [2/2]

void StaticGraph::shuffle_vertices ( const std::vector< verti > & perm )

Shuffle vertex indices by the given permutation. Vertex v becomes perm[v], for all v.

See also: ParityGame::shuffle

Definition at line 291 of file Graph.cpp.

◆ succ_begin()

const_iterator StaticGraph::succ_begin ( verti v ) const

inline

Returns an iterator pointing to the first successor of vertex v.

Definition at line 196 of file Graph.h.

◆ succ_end()

const_iterator StaticGraph::succ_end ( verti v ) const

inline

Returns an iterator pointing past the last successor of vertex v.

Definition at line 201 of file Graph.h.

◆ swap()

void StaticGraph::swap ( StaticGraph & g )

noexcept

Swaps the contents of this graph with another one.

Definition at line 554 of file Graph.cpp.

◆ V()

verti StaticGraph::V ( ) const

inline

Returns the number of vertices in the graph.

Definition at line 187 of file Graph.h.

◆ write_raw()

void StaticGraph::write_raw ( std::ostream & os ) const

Write raw graph data to output stream

Definition at line 513 of file Graph.cpp.

Friends And Related Symbol Documentation

◆ EdgeIterator

friend class EdgeIterator

friend

Definition at line 301 of file Graph.h.

◆ operator&

constexpr bool operator&	(	EdgeDirection	a,
		EdgeDirection	b
	)

friend

Definition at line 94 of file Graph.h.

◆ SmallProgressMeasures

friend class SmallProgressMeasures

friend

Definition at line 299 of file Graph.h.

Member Data Documentation

◆ E_

edgei StaticGraph::E_ = 0UL

private

number of edges

Definition at line 280 of file Graph.h.

◆ edge_dir_

EdgeDirection StaticGraph::edge_dir_

private

Direction of stored edges.

Definition at line 294 of file Graph.h.

◆ predecessor_index_

edgei * StaticGraph::predecessor_index_ = nullptr

private

Definition at line 291 of file Graph.h.

◆ predecessors_

verti * StaticGraph::predecessors_ = nullptr

private

Definition at line 286 of file Graph.h.

◆ successor_index_

edgei* StaticGraph::successor_index_ = nullptr

private

Indices into the successor/predecessor lists (of size V + 1). successor_index[i] is the lowest index of an edge in successors with a predecessor >= i; successor_index[V] is E.

Definition at line 291 of file Graph.h.

◆ successors_

verti* StaticGraph::successors_ = nullptr

private

Successor/predecessor lists (of size E). If edges are pairs of nodes (i,j), then successors is the list of successors (j's) obtained after sorting edges by predecessors (i's), and vice versa for predecessors.

Definition at line 286 of file Graph.h.

◆ V_

verti StaticGraph::V_ = 0UL

private

number of vertices

Definition at line 279 of file Graph.h.

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

pg/include/mcrl2/pg/Graph.h
pg/source/Graph.cpp
pg/include/mcrl2/pg/Graph_impl.h

Public Types

Public Member Functions

Protected Member Functions

Private Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ edge_list

Member Enumeration Documentation

◆ EdgeDirection

Constructor & Destructor Documentation

◆ StaticGraph() [1/2]

◆ ~StaticGraph()

◆ StaticGraph() [2/2]

Member Function Documentation

◆ assign() [1/2]

◆ assign() [2/2]

◆ clear()

◆ degree()

◆ E()

◆ edge_dir()

◆ empty()

◆ get_edges()

◆ has_pred()

◆ has_succ()

◆ indegree()

◆ make_random()

◆ make_random_clustered()

◆ make_random_scc()

◆ make_subgraph() [1/2]

◆ make_subgraph() [2/2]

◆ make_subgraph_threads()

◆ operator=()

◆ outdegree()

◆ pred_begin()

◆ pred_end()

◆ read_raw()

◆ remove_edges()

◆ reset()

◆ shuffle_vertices() [1/2]

◆ shuffle_vertices() [2/2]

◆ succ_begin()

◆ succ_end()

◆ swap()

◆ V()

◆ write_raw()

Friends And Related Symbol Documentation

◆ EdgeIterator

◆ operator&

◆ SmallProgressMeasures

Member Data Documentation

◆ E_

◆ edge_dir_

◆ predecessor_index_

◆ predecessors_

◆ successor_index_

◆ successors_

◆ V_