storm::solver::helper Namespace Reference

Classes
class	GSVIBackend
class	IIBackend
struct	IIData
class	IntervalIterationHelper
	Implements interval iteration. More...
class	OptimisticValueIterationHelper
	Implements Optimistic value iteration. More...
class	OVIBackend
class	RationalSearchHelper
	Implements rational search. More...
class	RSBackend
class	SchedulerTrackingBackend
class	SchedulerTrackingHelper
	Helper class to extract optimal scheduler choices from a MinMax equation system solution. More...
class	SoundValueIterationHelper
	Implements sound value iteration. More...
class	SVIBackend
class	ValueIterationHelper
class	ValueIterationOperator
	This class represents the Value Iteration Operator (also known as Bellman operator). More...
class	VIOperatorBackend

Enumerations
enum class	RSResult { InProgress , Converged , PrecisionExceeded }
enum class	SVIStage { Initial , y_less_1 , b_eq_d }

Functions
template<typename ValueType >
boost::optional< std::vector< uint64_t > >	computeTopologicalGroupOrdering (storm::storage::SparseMatrix< ValueType > const &matrix)
	Returns a reordering of the matrix row(groups) and columns such that we can solve the (minmax or linear) equation system in one go.
template<typename ValueType >
storm::storage::SparseMatrix< ValueType >	createReorderedMatrix (storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< uint64_t > const &newToOrigIndexMap, std::vector< std::pair< uint64_t, ValueType > > &bFactors)
	reorders the row group such that the i'th row of the new matrix corresponds to the order[i]'th row of the source matrix.
template<typename ValueType >
bool	checkConvergence (std::pair< std::vector< ValueType >, std::vector< ValueType > > const &xy, uint64_t &convergenceCheckState, std::function< void()> const &getNextConvergenceCheckState, bool relative, ValueType const &precision)
template<bool Relative, typename ValueType >
static ValueType	diff (ValueType const &oldValue, ValueType const &newValue)
template<bool Relative, typename ValueType >
void	guessCandidate (std::pair< std::vector< ValueType >, std::vector< ValueType > > &vu, ValueType const &guessValue, std::optional< ValueType > const &lowerBound, std::optional< ValueType > const &upperBound)

Enumeration Type Documentation

RSResult

enum class storm::solver::helper::RSResult

strong

Enumerator
InProgress
Converged
PrecisionExceeded

Definition at line 16 of file RationalSearchHelper.h.

SVIStage

enum class storm::solver::helper::SVIStage

strong

Enumerator
Initial
y_less_1
b_eq_d

Definition at line 29 of file SoundValueIterationHelper.cpp.

Function Documentation

checkConvergence()

template<typename ValueType >

bool storm::solver::helper::checkConvergence	(	std::pair< std::vector< ValueType >, std::vector< ValueType > > const &	xy,
		uint64_t &	convergenceCheckState,
		std::function< void()> const &	getNextConvergenceCheckState,
		bool	relative,
		ValueType const &	precision
	)

Definition at line 57 of file IntervalterationHelper.cpp.

computeTopologicalGroupOrdering()

template<typename ValueType >

boost::optional< std::vector< uint64_t > > storm::solver::helper::computeTopologicalGroupOrdering

(

storm::storage::SparseMatrix< ValueType > const &

matrix

)

Returns a reordering of the matrix row(groups) and columns such that we can solve the (minmax or linear) equation system in one go.

More precisely, let x be the result and i an arbitrary rowgroup index. Solving for rowgroup x[i] only requires knowledge of the result at rowgroups x[i+1], x[i+2], ...

Definition at line 20 of file AcyclicSolverHelper.h.

createReorderedMatrix()

template<typename ValueType >

storm::storage::SparseMatrix< ValueType > storm::solver::helper::createReorderedMatrix	(	storm::storage::SparseMatrix< ValueType > const &	matrix,
		std::vector< uint64_t > const &	newToOrigIndexMap,
		std::vector< std::pair< uint64_t, ValueType > > &	bFactors
	)

reorders the row group such that the i'th row of the new matrix corresponds to the order[i]'th row of the source matrix.

Also eliminates selfloops p>0 and inserts 1/p into the bFactors

Definition at line 77 of file AcyclicSolverHelper.h.

diff()

template<bool Relative, typename ValueType >

static ValueType storm::solver::helper::diff ( ValueType const &  oldValue, ValueType const &  newValue  )

static

Definition at line 15 of file OptimisticValueIterationHelper.cpp.

guessCandidate()

template<bool Relative, typename ValueType >

void storm::solver::helper::guessCandidate	(	std::pair< std::vector< ValueType >, std::vector< ValueType > > &	vu,
		ValueType const &	guessValue,
		std::optional< ValueType > const &	lowerBound,
		std::optional< ValueType > const &	upperBound
	)

Definition at line 86 of file OptimisticValueIterationHelper.cpp.