storm::modelchecker::internal Namespace Reference

Classes
struct	NormalFormData
class	WeightedReachabilityHelper
	A helper class that computes (weighted) reachability probabilities for a given MDP in normal form. More...

Enumerations
enum class	BisectionMethodBounds { Simple , Advanced }

Functions
template<typename ValueType >
void	eliminateEndComponents (storm::storage::BitVector possibleEcStates, bool addRowAtRepresentativeState, std::optional< uint64_t > representativeRowEntry, storm::storage::SparseMatrix< ValueType > &matrix, uint64_t &initialState, storm::storage::BitVector &rowsWithSum1, std::vector< ValueType > &rowValues1, storm::OptionalRef< std::vector< ValueType > > rowValues2={})
template<typename ValueType , typename SolutionType = ValueType>
SolutionType	solveMinMaxEquationSystem (storm::Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< ValueType > const &rowValues, storm::storage::BitVector const &rowsWithSum1, storm::solver::OptimizationDirection const dir, uint64_t const initialState)
template<typename ValueType >
void	computeReachabilityProbabilities (Environment const &env, std::map< uint64_t, ValueType > &nonZeroResults, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &allowedStates, storm::storage::BitVector const &targetStates)
	Computes the reachability probabilities for the given target states and inserts all non-zero values into the given map.
template<typename ValueType >
NormalFormData< ValueType >	obtainNormalForm (Environment const &env, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &relevantStates, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
template<typename ValueType , typename SolutionType = ValueType>
SolutionType	computeViaRestartMethod (Environment const &env, uint64_t const initialState, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, NormalFormData< ValueType > const &normalForm)
	Uses the restart method by Baier et al.
template<typename ValueType , typename SolutionType = ValueType>
SolutionType	computeViaBisection (Environment const &env, BisectionMethodBounds boundOption, uint64_t const initialState, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, NormalFormData< ValueType > const &normalForm)
template<typename ValueType , typename SolutionType = ValueType>
SolutionType	computeViaPolicyIteration (Environment const &env, uint64_t const initialState, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, NormalFormData< ValueType > const &normalForm)
template<typename ValueType , typename SolutionType = ValueType>
std::optional< SolutionType >	handleTrivialCases (uint64_t const initialState, NormalFormData< ValueType > const &normalForm)

Enumeration Type Documentation

BisectionMethodBounds

enum class storm::modelchecker::internal::BisectionMethodBounds

strong

Enumerator
Simple
Advanced

Definition at line 535 of file ConditionalHelper.cpp.

Function Documentation

computeReachabilityProbabilities()

template<typename ValueType >

void storm::modelchecker::internal::computeReachabilityProbabilities	(	Environment const &	env,
		std::map< uint64_t, ValueType > &	nonZeroResults,
		storm::solver::OptimizationDirection const	dir,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::BitVector const &	initialStates,
		storm::storage::BitVector const &	allowedStates,
		storm::storage::BitVector const &	targetStates
	)

Computes the reachability probabilities for the given target states and inserts all non-zero values into the given map.

Note

This code is optimized for cases where not all states are reachable from the initial states.

Definition at line 112 of file ConditionalHelper.cpp.

computeViaBisection()

template<typename ValueType , typename SolutionType = ValueType>

SolutionType storm::modelchecker::internal::computeViaBisection	(	Environment const &	env,
		BisectionMethodBounds	boundOption,
		uint64_t const	initialState,
		storm::solver::OptimizationDirection const	dir,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		NormalFormData< ValueType > const &	normalForm
	)

Definition at line 537 of file ConditionalHelper.cpp.

computeViaPolicyIteration()

template<typename ValueType , typename SolutionType = ValueType>

SolutionType storm::modelchecker::internal::computeViaPolicyIteration	(	Environment const &	env,
		uint64_t const	initialState,
		storm::solver::OptimizationDirection const	dir,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		NormalFormData< ValueType > const &	normalForm
	)

Definition at line 646 of file ConditionalHelper.cpp.

computeViaRestartMethod()

template<typename ValueType , typename SolutionType = ValueType>

SolutionType storm::modelchecker::internal::computeViaRestartMethod	(	Environment const &	env,
		uint64_t const	initialState,
		storm::solver::OptimizationDirection const	dir,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		NormalFormData< ValueType > const &	normalForm
	)

Uses the restart method by Baier et al.

See also

doi.org/10.1007/978-3-642-54862-8_43

Definition at line 226 of file ConditionalHelper.cpp.

eliminateEndComponents()

template<typename ValueType >

void storm::modelchecker::internal::eliminateEndComponents	(	storm::storage::BitVector	possibleEcStates,
		bool	addRowAtRepresentativeState,
		std::optional< uint64_t >	representativeRowEntry,
		storm::storage::SparseMatrix< ValueType > &	matrix,
		uint64_t &	initialState,
		storm::storage::BitVector &	rowsWithSum1,
		std::vector< ValueType > &	rowValues1,
		storm::OptionalRef< std::vector< ValueType > >	rowValues2 = {}
	)

Definition at line 30 of file ConditionalHelper.cpp.

handleTrivialCases()

template<typename ValueType , typename SolutionType = ValueType>

std::optional< SolutionType > storm::modelchecker::internal::handleTrivialCases	(	uint64_t const	initialState,
		NormalFormData< ValueType > const &	normalForm
	)

Definition at line 681 of file ConditionalHelper.cpp.

obtainNormalForm()

template<typename ValueType >

NormalFormData< ValueType > storm::modelchecker::internal::obtainNormalForm	(	Environment const &	env,
		storm::solver::OptimizationDirection const	dir,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	relevantStates,
		storm::storage::BitVector const &	targetStates,
		storm::storage::BitVector const &	conditionStates
	)

Definition at line 172 of file ConditionalHelper.cpp.

solveMinMaxEquationSystem()

template<typename ValueType , typename SolutionType = ValueType>

SolutionType storm::modelchecker::internal::solveMinMaxEquationSystem	(	storm::Environment const &	env,
		storm::storage::SparseMatrix< ValueType > const &	matrix,
		std::vector< ValueType > const &	rowValues,
		storm::storage::BitVector const &	rowsWithSum1,
		storm::solver::OptimizationDirection const	dir,
		uint64_t const	initialState
	)

Definition at line 87 of file ConditionalHelper.cpp.