storm::modelchecker::helper::internal::LraViHelper< ValueType, ComponentType, TransitionsType > Class Template Reference

Helper class that performs iterations of the value iteration method. More...

#include <LraViHelper.h>

Public Types
typedef std::function< ValueType(uint64_t)>	ValueGetter
	Function mapping from indices to values.

Public Member Functions
	LraViHelper (ComponentType const &component, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, ValueType const &aperiodicFactor, storm::storage::BitVector const *timedStates=nullptr, std::vector< ValueType > const *exitRates=nullptr)
	Initializes a new VI helper for the provided MEC or BSCC.
ValueType	performValueIteration (Environment const &env, ValueGetter const &stateValueGetter, ValueGetter const &actionValueGetter, std::vector< ValueType > const *exitRates=nullptr, storm::solver::OptimizationDirection const *dir=nullptr, std::vector< uint64_t > *choices=nullptr)
	Performs value iteration with the given state- and action values.

Detailed Description

template<typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
class storm::modelchecker::helper::internal::LraViHelper< ValueType, ComponentType, TransitionsType >

Helper class that performs iterations of the value iteration method.

The purpose of the template parameters ComponentType and TransitionsType are used to make this work for various model types.

See also

Ashok et al.: Value Iteration for Long-Run Average Reward in Markov Decision Processes (CAV'17), https://doi.org/10.1007/978-3-319-63387-9_10

Butkova, Wimmer, Hermanns: Long-Run Rewards for Markov Automata (TACAS'17), https://doi.org/10.1007/978-3-662-54580-5_11

Template Parameters

ValueType	The type of a value
ComponentType	The type of a 'bottom component' of the model (e.g. a BSCC (for purely deterministic models) or a MEC (for models with potential nondeterminism).
TransitionsType	The kind of transitions that occur.

Definition at line 42 of file LraViHelper.h.

Member Typedef Documentation

ValueGetter

template<typename ValueType , typename ComponentType , LraViTransitionsType TransitionsType>

typedef std::function<ValueType(uint64_t)> storm::modelchecker::helper::internal::LraViHelper< ValueType, ComponentType, TransitionsType >::ValueGetter

Function mapping from indices to values.

Definition at line 45 of file LraViHelper.h.

Constructor & Destructor Documentation

LraViHelper()

template<typename ValueType , typename ComponentType , LraViTransitionsType TransitionsType>

storm::modelchecker::helper::internal::LraViHelper< ValueType, ComponentType, TransitionsType >::LraViHelper	(	ComponentType const &	component,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		ValueType const &	aperiodicFactor,
		storm::storage::BitVector const *	timedStates = nullptr,
		std::vector< ValueType > const *	exitRates = nullptr
	)

Initializes a new VI helper for the provided MEC or BSCC.

Parameters

component	the MEC or BSCC
transitionMatrix	The transition matrix of the input model
aperiodicFactor	a non-zero factor that is used for making the MEC aperiodic (by adding selfloops to each state)
timedStates	States in which time can pass (Markovian states in a Markov automaton). If nullptr, it is assumed that all states are timed states
exitRates	The exit rates of the timed states (relevant for continuous time models). If nullptr, all rates are assumed to be 1 (which corresponds to a discrete time model)

Note

All indices and vectors must be w.r.t. the states as described by the provided transition matrix

Definition at line 25 of file LraViHelper.cpp.

Member Function Documentation

performValueIteration()

template<typename ValueType , typename ComponentType , LraViTransitionsType TransitionsType>

ValueType storm::modelchecker::helper::internal::LraViHelper< ValueType, ComponentType, TransitionsType >::performValueIteration	(	Environment const &	env,
		ValueGetter const &	stateValueGetter,
		ValueGetter const &	actionValueGetter,
		std::vector< ValueType > const *	exitRates = nullptr,
		storm::solver::OptimizationDirection const *	dir = nullptr,
		std::vector< uint64_t > *	choices = nullptr
	)

Performs value iteration with the given state- and action values.

Parameters

env	The environment, containing information on the precision of this computation.
stateValueGetter	function that returns for each state index (w.r.t. the input transition matrix) the reward for staying in state. Will only be called for timed states.
actionValueGetter	function that returns for each global choice index (w.r.t. the input transition matrix) the reward for taking that choice
exitRates	(as in the constructor)
dir	Optimization direction. Must be not nullptr in case of nondeterminism
choices	if not nullptr, the optimal choices will be inserted in this vector. The vector's size must then be equal to the number of row groups of the input transition matrix.

Returns

The (optimal) long run average value of the specified component.

Note

it is possible to call this method multiple times with different values. However, other changes to the environment or the optimization direction might not have the expected effect due to caching.

Definition at line 171 of file LraViHelper.cpp.

---

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

• src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h
• src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp