The flexible sparse matrix is used during state elimination. More...

#include <FlexibleSparseMatrix.h>

Public Types
typedef uint_fast64_t	index_type

typedef ValueType	value_type

typedef std::vector< storm::storage::MatrixEntry< index_type, value_type > >	row_type

typedef row_type::iterator	iterator

typedef row_type::const_iterator	const_iterator

Public Member Functions
	FlexibleSparseMatrix ()=default
	Constructs an empty flexible sparse matrix.

	FlexibleSparseMatrix (index_type rows)
	Constructs a flexible sparse matrix with rows many rows.

	FlexibleSparseMatrix (storm::storage::SparseMatrix< ValueType > const &matrix, bool setAllValuesToOne=false, bool revertEquationSystem=false)
	Constructs a flexible sparse matrix from a sparse matrix.

void	reserveInRow (index_type row, index_type numberOfElements)
	Reserves space for elements in row.

row_type &	getRow (index_type)
	Returns an object representing the given row.

row_type const &	getRow (index_type) const
	Returns an object representing the given row.

row_type &	getRow (index_type rowGroup, index_type offset)
	Returns an object representing the offset'th row in the rowgroup.

row_type const &	getRow (index_type rowGroup, index_type entryInGroup) const
	Returns an object representing the offset'th row in the rowgroup.

std::vector< index_type > const &	getRowGroupIndices () const
	Returns the grouping of rows of this matrix.

index_type	getRowCount () const
	Returns the number of rows of the matrix.

index_type	getColumnCount () const
	Returns the number of columns of the matrix.

index_type	getNonzeroEntryCount () const
	Returns the cached number of nonzero entries in the matrix.

index_type	getRowGroupCount () const
	Returns the number of row groups in the matrix.

index_type	getRowGroupSize (index_type group) const
	Returns the size of the given row group.

value_type	getRowSum (index_type row) const
	Computes the sum of the entries in a given row.

void	updateDimensions ()
	Recomputes the number of columns and the number of non-zero entries.

bool	empty () const
	Checks if the matrix has no elements.

bool	hasTrivialRowGrouping () const
	Retrieves whether the matrix has a (possibly) trivial row grouping.

void	filterEntries (storm::storage::BitVector const &rowConstraint, storm::storage::BitVector const &columnConstraint)
	Erases all entries whose row and column does not satisfy the given rowConstraint and the given columnConstraint.

storm::storage::SparseMatrix< ValueType >	createSparseMatrix ()
	Creates a sparse matrix from the flexible sparse matrix.

storm::storage::SparseMatrix< ValueType >	createSparseMatrix (storm::storage::BitVector const &rowConstraint, storm::storage::BitVector const &columnConstraint)
	Creates a sparse matrix from the flexible sparse matrix.

bool	rowHasDiagonalElement (storm::storage::sparse::state_type state)
	Checks whether the given state has a self-loop with an arbitrary probability in the probability matrix.

std::ostream &	printRow (std::ostream &out, index_type const &rowIndex) const
	Print row.

Friends
template<typename TPrime >
std::ostream &	operator<< (std::ostream &out, FlexibleSparseMatrix< TPrime > const &matrix)

Detailed Description

template<typename ValueType>
class storm::storage::FlexibleSparseMatrix< ValueType >

The flexible sparse matrix is used during state elimination.

Definition at line 21 of file FlexibleSparseMatrix.h.

Member Typedef Documentation

◆ const_iterator

template<typename ValueType >

typedef row_type::const_iterator storm::storage::FlexibleSparseMatrix< ValueType >::const_iterator

Definition at line 30 of file FlexibleSparseMatrix.h.

◆ index_type

template<typename ValueType >

typedef uint_fast64_t storm::storage::FlexibleSparseMatrix< ValueType >::index_type

Definition at line 26 of file FlexibleSparseMatrix.h.

◆ iterator

template<typename ValueType >

typedef row_type::iterator storm::storage::FlexibleSparseMatrix< ValueType >::iterator

Definition at line 29 of file FlexibleSparseMatrix.h.

◆ row_type

template<typename ValueType >

typedef std::vector<storm::storage::MatrixEntry<index_type, value_type> > storm::storage::FlexibleSparseMatrix< ValueType >::row_type

Definition at line 28 of file FlexibleSparseMatrix.h.

◆ value_type

template<typename ValueType >

typedef ValueType storm::storage::FlexibleSparseMatrix< ValueType >::value_type

Definition at line 27 of file FlexibleSparseMatrix.h.

Constructor & Destructor Documentation

◆ FlexibleSparseMatrix() [1/3]

template<typename ValueType >

storm::storage::FlexibleSparseMatrix< ValueType >::FlexibleSparseMatrix ( )

default

Constructs an empty flexible sparse matrix.

◆ FlexibleSparseMatrix() [2/3]

template<typename ValueType >

storm::storage::FlexibleSparseMatrix< ValueType >::FlexibleSparseMatrix ( index_type rows )

Constructs a flexible sparse matrix with rows many rows.

Parameters

rows	number of rows.

Definition at line 14 of file FlexibleSparseMatrix.cpp.

◆ FlexibleSparseMatrix() [3/3]

template<typename ValueType >

storm::storage::FlexibleSparseMatrix< ValueType >::FlexibleSparseMatrix	(	storm::storage::SparseMatrix< ValueType > const &	matrix,
		bool	setAllValuesToOne = `false`,
		bool	revertEquationSystem = `false`
	)

Constructs a flexible sparse matrix from a sparse matrix.

Parameters

matrix	Sparse matrix to construct from.
setAllValuesToOne	If true, all set entries are set to one. Default is false.
revertEquationSystem	If true, the matrix that will be created is the matrix (1-A), where A is the provided matrix.

Definition at line 19 of file FlexibleSparseMatrix.cpp.

Member Function Documentation

◆ createSparseMatrix() [1/2]

template<typename ValueType >

storm::storage::SparseMatrix< ValueType > storm::storage::FlexibleSparseMatrix< ValueType >::createSparseMatrix ( )

Creates a sparse matrix from the flexible sparse matrix.

Returns: The sparse matrix.

Definition at line 181 of file FlexibleSparseMatrix.cpp.

◆ createSparseMatrix() [2/2]

template<typename ValueType >

storm::storage::SparseMatrix< ValueType > storm::storage::FlexibleSparseMatrix< ValueType >::createSparseMatrix	(	storm::storage::BitVector const &	rowConstraint,
		storm::storage::BitVector const &	columnConstraint
	)

Creates a sparse matrix from the flexible sparse matrix.

Only the selected rows and columns will be considered. Empty rowGroups will be ignored

Parameters

rowConstraint	A bit vector indicating which rows to keep.
columnConstraint	A bit vector indicating which columns to keep.

Returns: The sparse matrix.

Definition at line 214 of file FlexibleSparseMatrix.cpp.

◆ empty()

template<typename ValueType >

bool storm::storage::FlexibleSparseMatrix< ValueType >::empty ( ) const

Checks if the matrix has no elements.

Returns: True, if the matrix is empty.

Definition at line 147 of file FlexibleSparseMatrix.cpp.

◆ filterEntries()

template<typename ValueType >

void storm::storage::FlexibleSparseMatrix< ValueType >::filterEntries	(	storm::storage::BitVector const &	rowConstraint,
		storm::storage::BitVector const &	columnConstraint
	)

Erases all entries whose row and column does not satisfy the given rowConstraint and the given columnConstraint.

Parameters

rowConstraint	A bit vector indicating which row entries to keep.
columnConstraint	A bit vector indicating which column entries to keep.

Definition at line 162 of file FlexibleSparseMatrix.cpp.

◆ getColumnCount()

template<typename ValueType >

FlexibleSparseMatrix< ValueType >::index_type storm::storage::FlexibleSparseMatrix< ValueType >::getColumnCount ( ) const

Returns the number of columns of the matrix.

Returns: The number of columns of the matrix.

Definition at line 105 of file FlexibleSparseMatrix.cpp.

◆ getNonzeroEntryCount()

template<typename ValueType >

FlexibleSparseMatrix< ValueType >::index_type storm::storage::FlexibleSparseMatrix< ValueType >::getNonzeroEntryCount ( ) const

Returns the cached number of nonzero entries in the matrix.

Returns: The number of nonzero entries in the matrix.

Definition at line 110 of file FlexibleSparseMatrix.cpp.

◆ getRow() [1/4]

template<typename ValueType >

FlexibleSparseMatrix< ValueType >::row_type const & storm::storage::FlexibleSparseMatrix< ValueType >::getRow	(	index_type	rowGroup,
		index_type	entryInGroup
	)		const

Returns an object representing the offset'th row in the rowgroup.

Parameters

rowGroup	the row group
offset	which row in the group

Returns: An object representing the given row.

Definition at line 88 of file FlexibleSparseMatrix.cpp.

◆ getRow() [2/4]

template<typename ValueType >

FlexibleSparseMatrix< ValueType >::row_type & storm::storage::FlexibleSparseMatrix< ValueType >::getRow	(	index_type	rowGroup,
		index_type	offset
	)

Returns an object representing the offset'th row in the rowgroup.

Parameters

rowGroup	the row group
offset	which row in the group

Returns: An object representing the given row.

Definition at line 81 of file FlexibleSparseMatrix.cpp.

◆ getRow() [3/4]

template<typename ValueType >

FlexibleSparseMatrix< ValueType >::row_type & storm::storage::FlexibleSparseMatrix< ValueType >::getRow ( index_type index )

Returns an object representing the given row.

Parameters

row	The row to get.

Returns: An object representing the given row.

Definition at line 71 of file FlexibleSparseMatrix.cpp.

◆ getRow() [4/4]

template<typename ValueType >

FlexibleSparseMatrix< ValueType >::row_type const & storm::storage::FlexibleSparseMatrix< ValueType >::getRow ( index_type index ) const

Returns an object representing the given row.

Parameters

row	The row to get.

Returns: An object representing the given row.

Definition at line 76 of file FlexibleSparseMatrix.cpp.

◆ getRowCount()

template<typename ValueType >

FlexibleSparseMatrix< ValueType >::index_type storm::storage::FlexibleSparseMatrix< ValueType >::getRowCount ( ) const

Returns the number of rows of the matrix.

Returns: The number of rows of the matrix.

Definition at line 100 of file FlexibleSparseMatrix.cpp.

◆ getRowGroupCount()

template<typename ValueType >

FlexibleSparseMatrix< ValueType >::index_type storm::storage::FlexibleSparseMatrix< ValueType >::getRowGroupCount ( ) const

Returns the number of row groups in the matrix.

Returns: The number of row groups in the matrix.

Definition at line 115 of file FlexibleSparseMatrix.cpp.

◆ getRowGroupIndices()

template<typename ValueType >

std::vector< typename FlexibleSparseMatrix< ValueType >::index_type > const & storm::storage::FlexibleSparseMatrix< ValueType >::getRowGroupIndices ( ) const

Returns the grouping of rows of this matrix.

Returns: The grouping of rows of this matrix.

Definition at line 95 of file FlexibleSparseMatrix.cpp.

◆ getRowGroupSize()

template<typename ValueType >

FlexibleSparseMatrix< ValueType >::index_type storm::storage::FlexibleSparseMatrix< ValueType >::getRowGroupSize ( index_type group ) const

Returns the size of the given row group.

Parameters

group The group whose size to retrieve.

Returns: The number of rows that belong to the given row group.

Definition at line 120 of file FlexibleSparseMatrix.cpp.

◆ getRowSum()

template<typename ValueType >

ValueType storm::storage::FlexibleSparseMatrix< ValueType >::getRowSum ( index_type row ) const

Computes the sum of the entries in a given row.

Parameters

row	The row that is to be summed.

Returns: The sum of the selected row.

Definition at line 125 of file FlexibleSparseMatrix.cpp.

◆ hasTrivialRowGrouping()

template<typename ValueType >

bool storm::storage::FlexibleSparseMatrix< ValueType >::hasTrivialRowGrouping ( ) const

Retrieves whether the matrix has a (possibly) trivial row grouping.

Returns: True iff the matrix has a (possibly) trivial row grouping.

Definition at line 157 of file FlexibleSparseMatrix.cpp.

◆ printRow()

template<typename ValueType >

std::ostream & storm::storage::FlexibleSparseMatrix< ValueType >::printRow	(	std::ostream &	out,
		index_type const &	rowIndex
	)		const

Print row.

Parameters

out	Output stream.
rowIndex	Index of row to print.

Returns: Output with printed row.

Definition at line 281 of file FlexibleSparseMatrix.cpp.

◆ reserveInRow()

template<typename ValueType >

void storm::storage::FlexibleSparseMatrix< ValueType >::reserveInRow	(	index_type	row,
		index_type	numberOfElements
	)

Reserves space for elements in row.

Parameters

row	Row to reserve in.
numberOfElements	Number of elements to reserve space for.

Definition at line 66 of file FlexibleSparseMatrix.cpp.

◆ rowHasDiagonalElement()

template<typename ValueType >

bool storm::storage::FlexibleSparseMatrix< ValueType >::rowHasDiagonalElement ( storm::storage::sparse::state_type state )

Checks whether the given state has a self-loop with an arbitrary probability in the probability matrix.

Parameters

state The state for which to check whether it possesses a self-loop.

Returns: True iff the given state has a self-loop with an arbitrary probability in the probability matrix.

Definition at line 267 of file FlexibleSparseMatrix.cpp.

◆ updateDimensions()

template<typename ValueType >

void storm::storage::FlexibleSparseMatrix< ValueType >::updateDimensions ( )

Recomputes the number of columns and the number of non-zero entries.

Definition at line 134 of file FlexibleSparseMatrix.cpp.

Friends And Related Symbol Documentation

◆ operator<<

template<typename ValueType >

template<typename TPrime >

std::ostream & operator<<	(	std::ostream &	out,
		FlexibleSparseMatrix< TPrime > const &	matrix
	)

friend

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

src/storm/solver/stateelimination/DynamicStatePriorityQueue.h
src/storm/storage/FlexibleSparseMatrix.h
src/storm/storage/FlexibleSparseMatrix.cpp

Public Types

Public Member Functions

Friends

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ index_type

◆ iterator

◆ row_type

◆ value_type

Constructor & Destructor Documentation

◆ FlexibleSparseMatrix() [1/3]

◆ FlexibleSparseMatrix() [2/3]

◆ FlexibleSparseMatrix() [3/3]

Member Function Documentation

◆ createSparseMatrix() [1/2]

◆ createSparseMatrix() [2/2]

◆ empty()

◆ filterEntries()

◆ getColumnCount()

◆ getNonzeroEntryCount()

◆ getRow() [1/4]

◆ getRow() [2/4]

◆ getRow() [3/4]

◆ getRow() [4/4]

◆ getRowCount()

◆ getRowGroupCount()

◆ getRowGroupIndices()

◆ getRowGroupSize()

◆ getRowSum()

◆ hasTrivialRowGrouping()

◆ printRow()

◆ reserveInRow()

◆ rowHasDiagonalElement()

◆ updateDimensions()

Friends And Related Symbol Documentation

◆ operator<<