storm::solver::helper Namespace Reference

Namespaces
namespace	gviinternal

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

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, std::optional< 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 17 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 21 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, std::optional< 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. A factor of std::nullopt marks a row with a selfloop of probability one. Such a row has no scaling factor at all: the equation for it can only be satisfied if the row contributes nothing, i.e. if the corresponding entry of the b vector is zero.

Definition at line 82 of file AcyclicSolverHelper.h.

diff()

template<bool Relative, typename ValueType>

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.