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

Functions
template<typename ValueType>
std::optional< typename storm::transformer::EndComponentEliminator< ValueType >::EndComponentEliminatorReturnType >	eliminateEndComponents (storm::storage::BitVector const &possibleEcStates, bool addRowAtRepresentativeState, std::optional< uint64_t > const representativeRowEntry, storm::storage::SparseMatrix< ValueType > &matrix, 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::SolveGoal< ValueType, SolutionType > const &goal, uint64_t const initialState, std::optional< std::vector< uint64_t > > &schedulerOutput)
template<typename ValueType>
std::unique_ptr< storm::storage::Scheduler< ValueType > >	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, bool computeScheduler=true)
	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, bool computeScheduler, 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>
void	finalizeSchedulerForMaybeStates (storm::storage::Scheduler< SolutionType > &scheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &maybeStatesWithoutChoice, storm::storage::BitVector const &maybeStatesWithChoice, std::vector< uint64_t > const &stateToFinalEc, NormalFormData< ValueType > const &normalForm, uint64_t initialComponentIndex, storm::storage::BitVector const &initialComponentExitStates, storm::storage::BitVector const &initialComponentExitRows, uint64_t chosenInitialComponentExitState, uint64_t chosenInitialComponentExit)
template<typename ValueType, typename SolutionType = ValueType>
internal::ResultReturnType< ValueType >	computeViaRestartMethod (Environment const &env, uint64_t const initialState, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, bool computeScheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, NormalFormData< ValueType > const &normalForm)
	Uses the restart method by Baier et al.
template<typename ValueType, typename SolutionType = ValueType>
internal::ResultReturnType< ValueType >	computeViaBisection (Environment const &env, bool const useAdvancedBounds, bool const usePolicyTracking, uint64_t const initialState, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, bool computeScheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, NormalFormData< ValueType > const &normalForm)
template<typename ValueType, typename SolutionType = ValueType>
internal::ResultReturnType< ValueType >	computeViaBisection (Environment const &env, ConditionalAlgorithmSetting const alg, uint64_t const initialState, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, bool computeScheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, NormalFormData< ValueType > const &normalForm)
template<typename ValueType, typename SolutionType = ValueType>
internal::ResultReturnType< ValueType >	decideThreshold (Environment const &env, uint64_t const initialState, storm::OptimizationDirection const &direction, SolutionType const &threshold, bool computeScheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, NormalFormData< ValueType > const &normalForm)
template<typename ValueType, typename SolutionType = ValueType>
internal::ResultReturnType< 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)

Function Documentation

◆ computeReachabilityProbabilities()

template<typename ValueType>

std::unique_ptr< storm::storage::Scheduler< ValueType > > 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,
		bool	computeScheduler = true )

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 137 of file ConditionalHelper.cpp.

◆ computeViaBisection() [1/2]

template<typename ValueType, typename SolutionType = ValueType>

internal::ResultReturnType< ValueType > storm::modelchecker::internal::computeViaBisection	(	Environment const &	env,
		bool const	useAdvancedBounds,
		bool const	usePolicyTracking,
		uint64_t const	initialState,
		storm::solver::SolveGoal< ValueType, SolutionType > const &	goal,
		bool	computeScheduler,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		NormalFormData< ValueType > const &	normalForm )

Definition at line 976 of file ConditionalHelper.cpp.

◆ computeViaBisection() [2/2]

template<typename ValueType, typename SolutionType = ValueType>

internal::ResultReturnType< ValueType > storm::modelchecker::internal::computeViaBisection	(	Environment const &	env,
		ConditionalAlgorithmSetting const	alg,
		uint64_t const	initialState,
		storm::solver::SolveGoal< ValueType, SolutionType > const &	goal,
		bool	computeScheduler,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		NormalFormData< ValueType > const &	normalForm )

Definition at line 1159 of file ConditionalHelper.cpp.

◆ computeViaPolicyIteration()

template<typename ValueType, typename SolutionType = ValueType>

internal::ResultReturnType< 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 1212 of file ConditionalHelper.cpp.

◆ computeViaRestartMethod()

template<typename ValueType, typename SolutionType = ValueType>

internal::ResultReturnType< ValueType > storm::modelchecker::internal::computeViaRestartMethod	(	Environment const &	env,
		uint64_t const	initialState,
		storm::solver::SolveGoal< ValueType, SolutionType > const &	goal,
		bool	computeScheduler,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		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 443 of file ConditionalHelper.cpp.

◆ decideThreshold()

template<typename ValueType, typename SolutionType = ValueType>

internal::ResultReturnType< ValueType > storm::modelchecker::internal::decideThreshold	(	Environment const &	env,
		uint64_t const	initialState,
		storm::OptimizationDirection const &	direction,
		SolutionType const &	threshold,
		bool	computeScheduler,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		NormalFormData< ValueType > const &	normalForm )

Definition at line 1174 of file ConditionalHelper.cpp.

◆ eliminateEndComponents()

template<typename ValueType>

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

Definition at line 36 of file ConditionalHelper.cpp.

◆ finalizeSchedulerForMaybeStates()

template<typename ValueType, typename SolutionType = ValueType>

void storm::modelchecker::internal::finalizeSchedulerForMaybeStates	(	storm::storage::Scheduler< SolutionType > &	scheduler,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	maybeStates,
		storm::storage::BitVector const &	maybeStatesWithoutChoice,
		storm::storage::BitVector const &	maybeStatesWithChoice,
		std::vector< uint64_t > const &	stateToFinalEc,
		NormalFormData< ValueType > const &	normalForm,
		uint64_t	initialComponentIndex,
		storm::storage::BitVector const &	initialComponentExitStates,
		storm::storage::BitVector const &	initialComponentExitRows,
		uint64_t	chosenInitialComponentExitState,
		uint64_t	chosenInitialComponentExit )

Definition at line 282 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 1249 of file ConditionalHelper.cpp.

◆ obtainNormalForm()

template<typename ValueType>

NormalFormData< ValueType > storm::modelchecker::internal::obtainNormalForm	(	Environment const &	env,
		storm::solver::OptimizationDirection const	dir,
		bool	computeScheduler,
		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 224 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::SolveGoal< ValueType, SolutionType > const &	goal,
		uint64_t const	initialState,
		std::optional< std::vector< uint64_t > > &	schedulerOutput )

Definition at line 93 of file ConditionalHelper.cpp.

Classes

Functions

Function Documentation

◆ computeReachabilityProbabilities()

◆ computeViaBisection() [1/2]

◆ computeViaBisection() [2/2]

◆ computeViaPolicyIteration()

◆ computeViaRestartMethod()

◆ decideThreshold()

◆ eliminateEndComponents()

◆ finalizeSchedulerForMaybeStates()

◆ handleTrivialCases()

◆ obtainNormalForm()

◆ solveMinMaxEquationSystem()