#include <Multiplier.h>

Inheritance diagram for storm::solver::Multiplier< ValueType, SolutionType >:

Public Member Functions
	Multiplier (storm::storage::SparseMatrix< ValueType > const &matrix)
virtual	~Multiplier ()=default
virtual void	clearCache () const
virtual void	multiply (Environment const &env, std::vector< SolutionType > const &x, std::vector< ValueType > const *b, std::vector< SolutionType > &result) const =0
	Performs a matrix-vector multiplication x' = A*x + b.
virtual void	multiplyGaussSeidel (Environment const &env, std::vector< SolutionType > &x, std::vector< ValueType > const *b, bool backwards=true) const =0
	Performs a matrix-vector multiplication in gauss-seidel style.
void	multiplyAndReduce (Environment const &env, OptimizationDirection const &dir, std::vector< SolutionType > const &x, std::vector< ValueType > const b, std::vector< SolutionType > &result, UncertaintyResolutionMode const &uncertaintyResolutionMode=UncertaintyResolutionMode::Unset, std::vector< uint_fast64_t > choices=nullptr) const
	Performs a matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.
virtual void	multiplyAndReduce (Environment const &env, OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< SolutionType > const &x, std::vector< ValueType > const b, std::vector< SolutionType > &result, UncertaintyResolutionMode const &uncertaintyResolutionMode=UncertaintyResolutionMode::Unset, std::vector< uint_fast64_t > choices=nullptr) const =0
void	multiplyAndReduceGaussSeidel (Environment const &env, OptimizationDirection const &dir, std::vector< SolutionType > &x, std::vector< ValueType > const b, std::vector< uint_fast64_t > choices=nullptr, bool backwards=true) const
	Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.
virtual void	multiplyAndReduceGaussSeidel (Environment const &env, OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< SolutionType > &x, std::vector< ValueType > const b, std::vector< uint_fast64_t > choices=nullptr, bool backwards=true) const =0
void	repeatedMultiply (Environment const &env, std::vector< SolutionType > &x, std::vector< ValueType > const *b, uint64_t n) const
	Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b.
void	repeatedMultiplyAndReduce (Environment const &env, OptimizationDirection const &dir, std::vector< SolutionType > &x, std::vector< ValueType > const *b, uint64_t n, UncertaintyResolutionMode const &uncertaintyResolutionMode=UncertaintyResolutionMode::Unset) const
	Performs repeated matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.
void	repeatedMultiplyWithFactor (Environment const &env, std::vector< SolutionType > &x, std::vector< ValueType > const *b, uint64_t n, SolutionType factor) const
	Performs repeated matrix-vector multiplication x' = A(factor x) + b.
void	repeatedMultiplyAndReduceWithFactor (Environment const &env, OptimizationDirection const &dir, std::vector< SolutionType > &x, std::vector< ValueType > const *b, uint64_t n, SolutionType factor, UncertaintyResolutionMode const &uncertaintyResolutionMode=UncertaintyResolutionMode::Unset) const
	Performs repeated matrix-vector multiplication x' = A(factor x) + b, minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.

Protected Member Functions
std::vector< SolutionType > &	provideCachedVector (uint64_t size) const

Protected Attributes
std::unique_ptr< std::vector< SolutionType > >	cachedVector
storm::storage::SparseMatrix< ValueType > const &	matrix

Detailed Description

template<typename ValueType, typename SolutionType = ValueType>
class storm::solver::Multiplier< ValueType, SolutionType >

Definition at line 22 of file Multiplier.h.

Constructor & Destructor Documentation

◆ Multiplier()

template<typename ValueType, typename SolutionType>

storm::solver::Multiplier< ValueType, SolutionType >::Multiplier ( storm::storage::SparseMatrix< ValueType > const & matrix )

Definition at line 22 of file Multiplier.cpp.

◆ ~Multiplier()

template<typename ValueType, typename SolutionType = ValueType>

virtual storm::solver::Multiplier< ValueType, SolutionType >::~Multiplier ( )

virtualdefault

Member Function Documentation

◆ clearCache()

template<typename ValueType, typename SolutionType>

void storm::solver::Multiplier< ValueType, SolutionType >::clearCache ( ) const

virtual

Reimplemented in storm::solver::ViOperatorMultiplier< ValueType, TrivialRowGrouping, SolutionType >.

Definition at line 27 of file Multiplier.cpp.

◆ multiply()

template<typename ValueType, typename SolutionType = ValueType>

virtual void storm::solver::Multiplier< ValueType, SolutionType >::multiply	(	Environment const &	env,
		std::vector< SolutionType > const &	x,
		std::vector< ValueType > const *	b,
		std::vector< SolutionType > &	result ) const

pure virtual

Performs a matrix-vector multiplication x' = A*x + b.

Parameters

x	The input vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
b	If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
result	The target vector into which to write the multiplication result. Its length must be equal to the number of rows of A. Can be the same as the x vector.

◆ multiplyAndReduce() [1/2]

template<typename ValueType, typename SolutionType>

void storm::solver::Multiplier< ValueType, SolutionType >::multiplyAndReduce	(	Environment const &	env,
		OptimizationDirection const &	dir,
		std::vector< SolutionType > const &	x,
		std::vector< ValueType > const *	b,
		std::vector< SolutionType > &	result,
		UncertaintyResolutionMode const &	uncertaintyResolutionMode = UncertaintyResolutionMode::Unset,
		std::vector< uint_fast64_t > *	choices = nullptr ) const

Performs a matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.

Parameters

dir	The direction for the reduction step.
rowGroupIndices	A vector storing the row groups over which to reduce.
x	The input vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
b	If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
result	The target vector into which to write the multiplication result. Its length must be equal to the number of rows of A. Can be the same as the x vector.
uncertaintyResolutionMode	The mode according to which to resolve uncertainty in the reduction step.
choices	If given, the choices made in the reduction process are written to this vector.

Definition at line 32 of file Multiplier.cpp.

◆ multiplyAndReduce() [2/2]

template<typename ValueType, typename SolutionType = ValueType>

virtual void storm::solver::Multiplier< ValueType, SolutionType >::multiplyAndReduce	(	Environment const &	env,
		OptimizationDirection const &	dir,
		std::vector< uint64_t > const &	rowGroupIndices,
		std::vector< SolutionType > const &	x,
		std::vector< ValueType > const *	b,
		std::vector< SolutionType > &	result,
		UncertaintyResolutionMode const &	uncertaintyResolutionMode = UncertaintyResolutionMode::Unset,
		std::vector< uint_fast64_t > *	choices = nullptr ) const

pure virtual

◆ multiplyAndReduceGaussSeidel() [1/2]

template<typename ValueType, typename SolutionType>

void storm::solver::Multiplier< ValueType, SolutionType >::multiplyAndReduceGaussSeidel	(	Environment const &	env,
		OptimizationDirection const &	dir,
		std::vector< SolutionType > &	x,
		std::vector< ValueType > const *	b,
		std::vector< uint_fast64_t > *	choices = nullptr,
		bool	backwards = true ) const

Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.

Parameters

dir	The direction for the reduction step.
rowGroupIndices	A vector storing the row groups over which to reduce.
x	The input/output vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
b	If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
result	The target vector into which to write the multiplication result. Its length must be equal to the number of rows of A. Can be the same as the x vector.
choices	If given, the choices made in the reduction process are written to this vector.
backwards	if true, the iterations will be performed beginning from the last rowgroup and ending at the first rowgroup.

Definition at line 40 of file Multiplier.cpp.

◆ multiplyAndReduceGaussSeidel() [2/2]

template<typename ValueType, typename SolutionType = ValueType>

virtual void storm::solver::Multiplier< ValueType, SolutionType >::multiplyAndReduceGaussSeidel	(	Environment const &	env,
		OptimizationDirection const &	dir,
		std::vector< uint64_t > const &	rowGroupIndices,
		std::vector< SolutionType > &	x,
		std::vector< ValueType > const *	b,
		std::vector< uint_fast64_t > *	choices = nullptr,
		bool	backwards = true ) const

pure virtual

◆ multiplyGaussSeidel()

template<typename ValueType, typename SolutionType = ValueType>

virtual void storm::solver::Multiplier< ValueType, SolutionType >::multiplyGaussSeidel	(	Environment const &	env,
		std::vector< SolutionType > &	x,
		std::vector< ValueType > const *	b,
		bool	backwards = true ) const

pure virtual

Performs a matrix-vector multiplication in gauss-seidel style.

Parameters

x	The input/output vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
b	If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
backwards	if true, the iterations will be performed beginning from the last row and ending at the first row.

◆ provideCachedVector()

template<typename ValueType, typename SolutionType>

std::vector< SolutionType > & storm::solver::Multiplier< ValueType, SolutionType >::provideCachedVector ( uint64_t size ) const

protected

Definition at line 116 of file Multiplier.cpp.

◆ repeatedMultiply()

template<typename ValueType, typename SolutionType>

void storm::solver::Multiplier< ValueType, SolutionType >::repeatedMultiply	(	Environment const &	env,
		std::vector< SolutionType > &	x,
		std::vector< ValueType > const *	b,
		uint64_t	n ) const

Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b.

After performing the necessary multiplications, the result is written to the input vector x. Note that the matrix A has to be given upon construction time of the solver object.

Parameters

x	The initial vector with which to perform matrix-vector multiplication. Its length must be equal to the number of columns of A.
b	If non-null, this vector is added after each multiplication. If given, its length must be equal to the number of rows of A.
n	The number of times to perform the multiplication.

Definition at line 47 of file Multiplier.cpp.

◆ repeatedMultiplyAndReduce()

template<typename ValueType, typename SolutionType>

void storm::solver::Multiplier< ValueType, SolutionType >::repeatedMultiplyAndReduce	(	Environment const &	env,
		OptimizationDirection const &	dir,
		std::vector< SolutionType > &	x,
		std::vector< ValueType > const *	b,
		uint64_t	n,
		UncertaintyResolutionMode const &	uncertaintyResolutionMode = UncertaintyResolutionMode::Unset ) const

Performs repeated matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.

Parameters

dir	The direction for the reduction step.
x	The input vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
b	If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
result	The target vector into which to write the multiplication result. Its length must be equal to the number of rows of A.
n	The number of times to perform the multiplication.
uncertaintyResolutionMode	The mode according to which to resolve uncertainty in the reduction step.

Definition at line 63 of file Multiplier.cpp.

◆ repeatedMultiplyAndReduceWithFactor()

template<typename ValueType, typename SolutionType>

void storm::solver::Multiplier< ValueType, SolutionType >::repeatedMultiplyAndReduceWithFactor	(	Environment const &	env,
		OptimizationDirection const &	dir,
		std::vector< SolutionType > &	x,
		std::vector< ValueType > const *	b,
		uint64_t	n,
		SolutionType	factor,
		UncertaintyResolutionMode const &	uncertaintyResolutionMode = UncertaintyResolutionMode::Unset ) const

Performs repeated matrix-vector multiplication x' = A*(factor * x) + b, minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.

Vector x is scaled by factor in each iteration.

Parameters

dir	The direction for the reduction step.
x	The input vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
b	If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
result	The target vector into which to write the multiplication result. Its length must be equal to the number of rows of A.
n	The number of times to perform the multiplication.
uncertaintyResolutionMode	The mode according to which to resolve uncertainty in the reduction step.
factor	The scalar to multiply with in each iteration.

Definition at line 80 of file Multiplier.cpp.

◆ repeatedMultiplyWithFactor()

template<typename ValueType, typename SolutionType>

void storm::solver::Multiplier< ValueType, SolutionType >::repeatedMultiplyWithFactor	(	Environment const &	env,
		std::vector< SolutionType > &	x,
		std::vector< ValueType > const *	b,
		uint64_t	n,
		SolutionType	factor ) const

Performs repeated matrix-vector multiplication x' = A*(factor * x) + b.

Vector x is scaled by factor in each iteration.

Parameters

x	The input vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
b	If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
result	The target vector into which to write the multiplication result. Its length must be equal to the number of rows of A.
n	The number of times to perform the multiplication.
factor	The scalar to multiply with in each iteration.

Definition at line 99 of file Multiplier.cpp.

Member Data Documentation

◆ cachedVector

template<typename ValueType, typename SolutionType = ValueType>

std::unique_ptr<std::vector<SolutionType> > storm::solver::Multiplier< ValueType, SolutionType >::cachedVector

mutableprotected

Definition at line 167 of file Multiplier.h.

◆ matrix

template<typename ValueType, typename SolutionType = ValueType>

storm::storage::SparseMatrix<ValueType> const& storm::solver::Multiplier< ValueType, SolutionType >::matrix

protected

Definition at line 168 of file Multiplier.h.

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

src/storm/solver/multiplier/Multiplier.h
src/storm/solver/multiplier/Multiplier.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Multiplier()

◆ ~Multiplier()

Member Function Documentation

◆ clearCache()

◆ multiply()

◆ multiplyAndReduce() [1/2]

◆ multiplyAndReduce() [2/2]

◆ multiplyAndReduceGaussSeidel() [1/2]

◆ multiplyAndReduceGaussSeidel() [2/2]

◆ multiplyGaussSeidel()

◆ provideCachedVector()

◆ repeatedMultiply()

◆ repeatedMultiplyAndReduce()

◆ repeatedMultiplyAndReduceWithFactor()

◆ repeatedMultiplyWithFactor()

Member Data Documentation

◆ cachedVector

◆ matrix