Typedefs
using	index_type = uint64_t

Enumerations
enum class	OrderKind { Bfs , Dfs , ReverseBfs , ReverseDfs , Random }
	The order in which the states of a matrix are visited in a depth-first search or breadth-first search traversal. More...

Functions
std::string	orderKindtoString (OrderKind order)
	Converts the given order to a string.

OrderKind	orderKindFromString (std::string const &order)
	Gets the order from the given string.

std::vector< std::string >	orderKinds ()
	Returns a list of possible order kinds.

std::vector< index_type >	createRandomPermutation (index_type size)
	Creates a random (uniformly distributed) permutation of the given size.

std::vector< index_type >	createRandomPermutation (index_type size, index_type seed)
	Creates a random (uniformly distributed) permutation of the given size.

template<typename ValueType >
std::vector< index_type >	createPermutation (OrderKind order, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &initialStates)
	Creates a permutation that orders the states of the given matrix in the given exploration order.

std::vector< index_type >	invertPermutation (std::vector< index_type > const &permutation)
	Inverts the given permutation.

void	reversePermutationInPlace (std::vector< index_type > &permutation)
	Reverses the given permutation.

bool	isValidPermutation (std::vector< index_type > const &permutation)
	Returns true if the given vector is a permutation of the numbers 0, 1, ..., n-1 for n = permutation.size().

template std::vector< index_type >	createPermutation (OrderKind order, storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::BitVector const &initialStates)

template std::vector< index_type >	createPermutation (OrderKind order, storm::storage::SparseMatrix< storm::RationalNumber > const &transitionMatrix, storm::storage::BitVector const &initialStates)

template std::vector< index_type >	createPermutation (OrderKind order, storm::storage::SparseMatrix< storm::RationalFunction > const &transitionMatrix, storm::storage::BitVector const &initialStates)

Typedef Documentation

◆ index_type

using storm::utility::permutation::index_type = typedef uint64_t

Definition at line 16 of file permutation.h.

Enumeration Type Documentation

◆ OrderKind

enum class storm::utility::permutation::OrderKind

strong

The order in which the states of a matrix are visited in a depth-first search or breadth-first search traversal.

Enumerator
Bfs
Dfs
ReverseBfs
ReverseDfs
Random

Definition at line 21 of file permutation.h.

Function Documentation

◆ createPermutation() [1/4]

template std::vector< index_type > storm::utility::permutation::createPermutation	(	OrderKind	order,
		storm::storage::SparseMatrix< double > const &	transitionMatrix,
		storm::storage::BitVector const &	initialStates
	)

◆ createPermutation() [2/4]

template std::vector< index_type > storm::utility::permutation::createPermutation	(	OrderKind	order,
		storm::storage::SparseMatrix< storm::RationalFunction > const &	transitionMatrix,
		storm::storage::BitVector const &	initialStates
	)

◆ createPermutation() [3/4]

template std::vector< index_type > storm::utility::permutation::createPermutation	(	OrderKind	order,
		storm::storage::SparseMatrix< storm::RationalNumber > const &	transitionMatrix,
		storm::storage::BitVector const &	initialStates
	)

◆ createPermutation() [4/4]

template<typename ValueType >

std::vector< index_type > storm::utility::permutation::createPermutation	(	OrderKind	order,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::BitVector const &	initialStates
	)

Creates a permutation that orders the states of the given matrix in the given exploration order.

Note: the resulting permutation will only contain those states that are reachable from the initial states.

Example: Let permutation[i_0] = 0, permutation[i_1] = 1, ..., permutation[i_n-1] = n-1. i_0 is the firs initial state. If the order is Dfs, i_1 is a successor of i_0, i_2 is a successor of i_1, etc. (assuming those successors exist). If the order is Bfs, i_1 is the second initial state, ...

Precondition: initialStates.size() == transitionMatrix.getRowGroupCount() == transitionMatrix.getColumnCount()

Definition at line 69 of file permutation.cpp.

◆ createRandomPermutation() [1/2]

std::vector< index_type > storm::utility::permutation::createRandomPermutation ( index_type size )

Creates a random (uniformly distributed) permutation of the given size.

Definition at line 54 of file permutation.cpp.

◆ createRandomPermutation() [2/2]

std::vector< index_type > storm::utility::permutation::createRandomPermutation	(	index_type	size,
		index_type	seed
	)

Creates a random (uniformly distributed) permutation of the given size.

It is guaranteed that the same seed will always produce the same permutation.

Definition at line 59 of file permutation.cpp.

◆ invertPermutation()

std::vector< index_type > storm::utility::permutation::invertPermutation ( std::vector< index_type > const & permutation )

Inverts the given permutation.

Returns: a vector v such that v[permutation[i]] == permutation[v[i]] == i for all i.

Definition at line 106 of file permutation.cpp.

◆ isValidPermutation()

bool storm::utility::permutation::isValidPermutation ( std::vector< index_type > const & permutation )

Returns true if the given vector is a permutation of the numbers 0, 1, ..., n-1 for n = permutation.size().

In other words, every integer from 0 to n-1 occurs exactly once in the vector.

Definition at line 121 of file permutation.cpp.

◆ orderKindFromString()

OrderKind storm::utility::permutation::orderKindFromString ( std::string const & order )

Gets the order from the given string.

Definition at line 36 of file permutation.cpp.

◆ orderKinds()

std::vector< std::string > storm::utility::permutation::orderKinds ( )

Returns a list of possible order kinds.

Definition at line 46 of file permutation.cpp.

◆ orderKindtoString()

std::string storm::utility::permutation::orderKindtoString ( OrderKind order )

Converts the given order to a string.

Definition at line 19 of file permutation.cpp.

◆ reversePermutationInPlace()

void storm::utility::permutation::reversePermutationInPlace ( std::vector< index_type > & permutation )

Reverses the given permutation.

Note: this does not reverse the given vector, but the permutation itself.

Returns: a vector v such that v[i] == permutation.size() - 1 - permutation[i] for all i.

Definition at line 114 of file permutation.cpp.

Typedefs

Enumerations

Functions