Namespaces
namespace	detail
namespace	internal
namespace	lexicographic
namespace	rewardbounded

Classes
class	HybridCtmcCslHelper
class	HybridMarkovAutomatonCslHelper
class	SparseCtmcCslHelper
class	UnifPlusHelper
class	SparseMarkovAutomatonCslHelper
class	DiscountingHelper
class	SparseStepBoundedHorizonHelper
class	SparseDeterministicVisitingTimesHelper
	Helper class for computing for each state the expected number of times to visit that state assuming a given initial distribution. More...
class	SparseInfiniteHorizonHelper
	Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. More...
class	HybridInfiniteHorizonHelper
	Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. More...
class	SparseDeterministicInfiniteHorizonHelper
	Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. More...
class	SparseNondeterministicInfiniteHorizonHelper
	Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. More...
class	SparseLTLHelper
	Helper class for LTL model checking. More...
class	ModelCheckerHelper
	Helper class for solving a model checking query. More...
class	SingleValueModelCheckerHelper
	Helper for model checking queries where we are interested in (optimizing) a single value per state. More...
class	BaierUpperRewardBoundsComputer
class	DsMpiDtmcPriorityLess
class	DsMpiMdpPriorityLess
class	DsMpiDtmcUpperRewardBoundsComputer
class	DsMpiMdpUpperRewardBoundsComputer
struct	DTMCSparseModelCheckingHelperReturnType
	The outcome of a quantitative model checking query on a sparse DTMC. More...
class	HybridDtmcPrctlHelper
struct	SolverRequirementsData
class	HybridMdpPrctlHelper
struct	MDPSparseModelCheckingHelperReturnType
class	SparseDtmcPrctlHelper
class	SparseMdpEndComponentInformation
struct	SparseMdpHintType
struct	MaybeStateResult
struct	QualitativeStateSetsUntilProbabilities
struct	QualitativeStateSetsReachabilityRewards
class	SparseMdpPrctlHelper
class	SymbolicDtmcPrctlHelper
class	SymbolicMdpPrctlHelper

Enumerations
enum class	SemanticSolutionType { UntilProbabilities , ExpectedRewards }
enum class	EquationSystemType { UntilProbabilities , ExpectedRewards }

Functions
template<storm::dd::DdType DdType, class ValueType>
void	discretizeRewardModel (typename storm::models::symbolic::Model< DdType, ValueType >::RewardModelType &rewardModel, storm::dd::Add< DdType, ValueType > const &exitRateVector, storm::dd::Bdd< DdType > const &markovianStates)
template<typename ValueType>
std::unique_ptr< storm::solver::MinMaxLinearEquationSolver< ValueType > >	setUpProbabilisticStatesSolver (storm::Environment &env, OptimizationDirection dir, storm::storage::SparseMatrix< ValueType > const &transitions)
template<typename ValueType>
void	computeBoundedReachabilityProbabilitiesImca (Environment const &env, OptimizationDirection dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &exitRates, storm::storage::BitVector const &goalStates, storm::storage::BitVector const &markovianNonGoalStates, storm::storage::BitVector const &probabilisticNonGoalStates, std::vector< ValueType > &markovianNonGoalValues, std::vector< ValueType > &probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps)
template<typename ValueType>
std::vector< ValueType >	computeBoundedUntilProbabilitiesImca (Environment const &env, OptimizationDirection dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &exitRateVector, storm::storage::BitVector const &markovianStates, storm::storage::BitVector const &psiStates, std::pair< double, std::optional< double > > const &boundsPair)
template<typename ValueType>
std::vector< ValueType >	computeUpperBoundsForExpectedVisitingTimes (storm::storage::SparseMatrix< ValueType > const &nonBsccMatrix, std::vector< ValueType > const &toBsccProbabilities)
template<>
std::vector< storm::RationalFunction >	computeUpperBoundsForExpectedVisitingTimes (storm::storage::SparseMatrix< storm::RationalFunction > const &, std::vector< storm::RationalFunction > const &)
template<typename ValueType>
void	addSspMatrixChoice (uint64_t const &inputMatrixChoice, storm::storage::SparseMatrix< ValueType > const &inputTransitionMatrix, std::vector< uint64_t > const &inputToSspStateMap, uint64_t const &numberOfNonComponentStates, uint64_t const &currentSspChoice, storm::storage::SparseMatrixBuilder< ValueType > &sspMatrixBuilder)
	Auxiliary function that adds the entries of the Ssp Matrix for a single choice (i.e., row) Transitions that lead to a Component state will be redirected to a new auxiliary state (there is one aux.
template<typename HelperType, typename FormulaType, typename ModelType>
void	setInformationFromCheckTaskNondeterministic (HelperType &helper, storm::modelchecker::CheckTask< FormulaType, typename ModelType::ValueType > const &checkTask, ModelType const &model)
	Forwards relevant information stored in the given CheckTask to the given helper.
template<typename HelperType, typename FormulaType, typename ModelType>
void	setInformationFromCheckTaskDeterministic (HelperType &helper, storm::modelchecker::CheckTask< FormulaType, typename ModelType::ValueType > const &checkTask, ModelType const &model)
	Forwards relevant information stored in the given CheckTask to the given helper.
template<typename TargetHelperType, typename SourceHelperType>
void	setInformationFromOtherHelperNondeterministic (TargetHelperType &targetHelper, SourceHelperType const &sourceHelperType, std::function< typename TargetHelperType::StateSet(typename SourceHelperType::StateSet const &)> const &stateSetTransformer)
	Forwards relevant information stored in another helper to the given helper.
template<typename TargetHelperType, typename SourceHelperType>
void	setInformationFromOtherHelperDeterministic (TargetHelperType &targetHelper, SourceHelperType const &sourceHelperType, std::function< typename TargetHelperType::StateSet(typename SourceHelperType::StateSet const &)> const &stateSetTransformer)
	Forwards relevant information stored in another helper to the given helper.
template<typename ValueType>
std::vector< ValueType >	computeUpperRewardBounds (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &rewards, std::vector< ValueType > const &oneStepTargetProbabilities)
template<>
std::vector< storm::RationalFunction >	computeUpperRewardBounds (storm::storage::SparseMatrix< storm::RationalFunction > const &transitionMatrix, std::vector< storm::RationalFunction > const &rewards, std::vector< storm::RationalFunction > const &oneStepTargetProbabilities)
template<typename ValueType>
void	expandSolutionAfterEndComponentElimination (SolverRequirementsData< ValueType > &solverRequirementsData, std::vector< ValueType > &x)
	Lifts the solution of an equation system in which end components have been eliminated back to the proper maybe states.
template<typename ValueType>
std::vector< uint64_t >	computeValidInitialSchedulerForUntilProbabilities (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &b)
template<typename ValueType>
void	eliminateExtendedStatesFromExplicitRepresentation (std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > &explicitRepresentation, boost::optional< std::vector< uint64_t > > &scheduler, storm::storage::BitVector const &properMaybeStates)
template<typename ValueType>
void	eliminateEndComponentsAndExtendedStatesUntilProbabilities (std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > &explicitRepresentation, SolverRequirementsData< ValueType > &solverRequirementsData, storm::storage::BitVector const &targetStates)
template<typename ValueType>
storm::storage::BitVector	computeTargetStatesForReachabilityRewardsFromExplicitRepresentation (storm::storage::SparseMatrix< ValueType > const &transitionMatrix)
template<typename ValueType>
std::vector< uint64_t >	computeValidInitialSchedulerForReachabilityRewards (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &properMaybeStates, storm::storage::BitVector const &targetStates)
template<typename ValueType>
std::vector< ValueType >	computeOneStepTargetProbabilitiesFromExtendedExplicitRepresentation (storm::storage::SparseMatrix< ValueType > const &extendedMatrix, storm::storage::BitVector const &properMaybeStates, storm::storage::BitVector const &targetStates)
template<typename ValueType>
void	eliminateEndComponentsAndTargetStatesReachabilityRewards (std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > &explicitRepresentation, SolverRequirementsData< ValueType > &solverRequirementsData, storm::storage::BitVector const &targetStates, bool computeOneStepTargetProbabilities)
template<typename ValueType>
void	setUpperRewardBounds (storm::solver::MinMaxLinearEquationSolver< ValueType > &solver, storm::OptimizationDirection const &direction, storm::storage::SparseMatrix< ValueType > const &submatrix, std::vector< ValueType > const &choiceRewards, std::vector< ValueType > const &oneStepTargetProbabilities)
template<typename ValueType, typename SolutionType>
std::vector< SolutionType >	computeRobustValuesForMaybeStates (Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > &&submatrix, std::vector< ValueType > const &b, bool computeReward, storm::solver::SolutionBounds< SolutionType > &solutionBounds)
template<typename ValueType, typename SolutionType>
std::vector< SolutionType >	computeUpperRewardBounds (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &rewards, std::vector< SolutionType > const &oneStepTargetProbabilities)
template<>
std::vector< storm::RationalFunction >	computeUpperRewardBounds (storm::storage::SparseMatrix< storm::RationalFunction > const &, std::vector< storm::RationalFunction > const &, std::vector< storm::RationalFunction > const &)
template<typename ValueType, typename SolutionType = ValueType>
std::vector< uint_fast64_t >	computeValidSchedulerHint (Environment const &env, SemanticSolutionType const &type, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &filterStates, storm::storage::BitVector const &targetStates, boost::optional< storm::storage::BitVector > const &selectedChoices)
template<typename ValueType, typename SolutionType>
void	extractValueAndSchedulerHint (SparseMdpHintType< SolutionType > &hintStorage, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, boost::optional< storm::storage::BitVector > const &selectedChoices, ModelCheckerHint const &hint, bool skipECWithinMaybeStatesCheck)
template<typename ValueType, typename SolutionType>
SparseMdpHintType< SolutionType >	computeHints (Environment const &env, SemanticSolutionType const &type, ModelCheckerHint const &hint, storm::OptimizationDirection const &dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &targetStates, bool produceScheduler, boost::optional< storm::storage::BitVector > const &selectedChoices=boost::none, bool hasUniqueSolution=false)
template<typename ValueType, typename SolutionType>
MaybeStateResult< SolutionType >	computeValuesForMaybeStates (Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > &&submatrix, std::vector< ValueType > const &b, bool produceScheduler, SparseMdpHintType< SolutionType > &hint)
template<typename ValueType>
QualitativeStateSetsUntilProbabilities	getQualitativeStateSetsUntilProbabilitiesFromHint (ModelCheckerHint const &hint)
template<typename ValueType, typename SolutionType>
QualitativeStateSetsUntilProbabilities	computeQualitativeStateSetsUntilProbabilities (storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
template<typename ValueType, typename SolutionType>
QualitativeStateSetsUntilProbabilities	getQualitativeStateSetsUntilProbabilities (storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, ModelCheckerHint const &hint)
template<typename SolutionType, bool subChoicesCoverOnlyMaybeStates = true>
void	extractSchedulerChoices (storm::storage::Scheduler< SolutionType > &scheduler, std::vector< uint64_t > const &subChoices, storm::storage::BitVector const &maybeStates)
template<typename ValueType, typename SolutionType>
void	extendScheduler (storm::storage::Scheduler< SolutionType > &scheduler, bool minimize, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
template<typename ValueType, typename SolutionType>
void	computeFixedPointSystemUntilProbabilities (storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b)
template<typename ValueType, typename SolutionType>
boost::optional< SparseMdpEndComponentInformation< ValueType > >	computeFixedPointSystemUntilProbabilitiesEliminateEndComponents (storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, bool produceScheduler)
template<typename ValueType>
QualitativeStateSetsReachabilityRewards	getQualitativeStateSetsReachabilityRewardsFromHint (ModelCheckerHint const &hint, storm::storage::BitVector const &targetStates)
template<typename ValueType, typename SolutionType>
QualitativeStateSetsReachabilityRewards	computeQualitativeStateSetsReachabilityRewards (Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, std::function< storm::storage::BitVector()> const &zeroRewardStatesGetter, std::function< storm::storage::BitVector()> const &zeroRewardChoicesGetter)
template<typename ValueType, typename SolutionType>
QualitativeStateSetsReachabilityRewards	getQualitativeStateSetsReachabilityRewards (Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, ModelCheckerHint const &hint, std::function< storm::storage::BitVector()> const &zeroRewardStatesGetter, std::function< storm::storage::BitVector()> const &zeroRewardChoicesGetter)
template<typename ValueType, typename SolutionType>
void	extendScheduler (storm::storage::Scheduler< SolutionType > &scheduler, bool minimize, QualitativeStateSetsReachabilityRewards const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, std::function< storm::storage::BitVector()> const &zeroRewardChoicesGetter)
template<typename ValueType, typename SolutionType>
void	extractSchedulerChoices (storm::storage::Scheduler< SolutionType > &scheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint_fast64_t > const &subChoices, storm::storage::BitVector const &maybeStates, boost::optional< storm::storage::BitVector > const &selectedChoices)
template<typename ValueType, typename SolutionType>
void	computeFixedPointSystemReachabilityRewards (storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, QualitativeStateSetsReachabilityRewards const &qualitativeStateSets, boost::optional< storm::storage::BitVector > const &selectedChoices, std::function< std::vector< ValueType >(uint_fast64_t, storm::storage::SparseMatrix< ValueType > const &, storm::storage::BitVector const &)> const &totalStateRewardVectorGetter, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, std::vector< ValueType > *oneStepTargetProbabilities=nullptr)
template<typename ValueType, typename SolutionType>
boost::optional< SparseMdpEndComponentInformation< ValueType > >	computeFixedPointSystemReachabilityRewardsEliminateEndComponents (storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, QualitativeStateSetsReachabilityRewards const &qualitativeStateSets, boost::optional< storm::storage::BitVector > const &selectedChoices, std::function< std::vector< ValueType >(uint_fast64_t, storm::storage::SparseMatrix< ValueType > const &, storm::storage::BitVector const &)> const &totalStateRewardVectorGetter, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, boost::optional< std::vector< ValueType > > &oneStepTargetProbabilities, bool produceScheduler)
template<typename ValueType, typename SolutionType>
void	computeUpperRewardBounds (SparseMdpHintType< SolutionType > &hintInformation, storm::OptimizationDirection const &direction, storm::storage::SparseMatrix< ValueType > const &submatrix, std::vector< ValueType > const &choiceRewards, std::vector< ValueType > const &oneStepTargetProbabilities)
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd< DdType >	computeValidSchedulerHint (EquationSystemType const &type, storm::models::symbolic::NondeterministicModel< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &transitionMatrix, storm::dd::Bdd< DdType > const &maybeStates, storm::dd::Bdd< DdType > const &targetStates)

Enumeration Type Documentation

◆ EquationSystemType

enum class storm::modelchecker::helper::EquationSystemType

strong

Enumerator
UntilProbabilities
ExpectedRewards

Definition at line 27 of file SymbolicMdpPrctlHelper.cpp.

◆ SemanticSolutionType

enum class storm::modelchecker::helper::SemanticSolutionType

strong

Enumerator
UntilProbabilities
ExpectedRewards

Definition at line 6 of file SemanticSolutionType.h.

Function Documentation

◆ addSspMatrixChoice()

template<typename ValueType>

void storm::modelchecker::helper::addSspMatrixChoice	(	uint64_t const &	inputMatrixChoice,
		storm::storage::SparseMatrix< ValueType > const &	inputTransitionMatrix,
		std::vector< uint64_t > const &	inputToSspStateMap,
		uint64_t const &	numberOfNonComponentStates,
		uint64_t const &	currentSspChoice,
		storm::storage::SparseMatrixBuilder< ValueType > &	sspMatrixBuilder )

Auxiliary function that adds the entries of the Ssp Matrix for a single choice (i.e., row) Transitions that lead to a Component state will be redirected to a new auxiliary state (there is one aux.

state for each component). Transitions that don't lead to a Component state are copied (taking a state index mapping into account).

Definition at line 392 of file SparseNondeterministicInfiniteHorizonHelper.cpp.

◆ computeBoundedReachabilityProbabilitiesImca()

template<typename ValueType>

void storm::modelchecker::helper::computeBoundedReachabilityProbabilitiesImca	(	Environment const &	env,
		OptimizationDirection	dir,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		std::vector< ValueType > const &	exitRates,
		storm::storage::BitVector const &	goalStates,
		storm::storage::BitVector const &	markovianNonGoalStates,
		storm::storage::BitVector const &	probabilisticNonGoalStates,
		std::vector< ValueType > &	markovianNonGoalValues,
		std::vector< ValueType > &	probabilisticNonGoalValues,
		ValueType	delta,
		uint64_t	numberOfSteps )

Definition at line 511 of file SparseMarkovAutomatonCslHelper.cpp.

◆ computeBoundedUntilProbabilitiesImca()

template<typename ValueType>

std::vector< ValueType > storm::modelchecker::helper::computeBoundedUntilProbabilitiesImca	(	Environment const &	env,
		OptimizationDirection	dir,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		std::vector< ValueType > const &	exitRateVector,
		storm::storage::BitVector const &	markovianStates,
		storm::storage::BitVector const &	psiStates,
		std::pair< double, std::optional< double > > const &	boundsPair )

Definition at line 635 of file SparseMarkovAutomatonCslHelper.cpp.

◆ computeFixedPointSystemReachabilityRewards()

template<typename ValueType, typename SolutionType>

void storm::modelchecker::helper::computeFixedPointSystemReachabilityRewards	(	storm::solver::SolveGoal< ValueType, SolutionType > &	goal,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		QualitativeStateSetsReachabilityRewards const &	qualitativeStateSets,
		boost::optional< storm::storage::BitVector > const &	selectedChoices,
		std::function< std::vector< ValueType >(uint_fast64_t, storm::storage::SparseMatrix< ValueType > const &, storm::storage::BitVector const &)> const &	totalStateRewardVectorGetter,
		storm::storage::SparseMatrix< ValueType > &	submatrix,
		std::vector< ValueType > &	b,
		std::vector< ValueType > *	oneStepTargetProbabilities = nullptr )

Definition at line 1252 of file SparseMdpPrctlHelper.cpp.

◆ computeFixedPointSystemReachabilityRewardsEliminateEndComponents()

template<typename ValueType, typename SolutionType>

boost::optional< SparseMdpEndComponentInformation< ValueType > > storm::modelchecker::helper::computeFixedPointSystemReachabilityRewardsEliminateEndComponents	(	storm::solver::SolveGoal< ValueType, SolutionType > &	goal,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		QualitativeStateSetsReachabilityRewards const &	qualitativeStateSets,
		boost::optional< storm::storage::BitVector > const &	selectedChoices,
		std::function< std::vector< ValueType >(uint_fast64_t, storm::storage::SparseMatrix< ValueType > const &, storm::storage::BitVector const &)> const &	totalStateRewardVectorGetter,
		storm::storage::SparseMatrix< ValueType > &	submatrix,
		std::vector< ValueType > &	b,
		boost::optional< std::vector< ValueType > > &	oneStepTargetProbabilities,
		bool	produceScheduler )

Definition at line 1311 of file SparseMdpPrctlHelper.cpp.

◆ computeFixedPointSystemUntilProbabilities()

template<typename ValueType, typename SolutionType>

void storm::modelchecker::helper::computeFixedPointSystemUntilProbabilities	(	storm::solver::SolveGoal< ValueType, SolutionType > &	goal,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		QualitativeStateSetsUntilProbabilities const &	qualitativeStateSets,
		storm::storage::SparseMatrix< ValueType > &	submatrix,
		std::vector< ValueType > &	b )

Definition at line 612 of file SparseMdpPrctlHelper.cpp.

◆ computeFixedPointSystemUntilProbabilitiesEliminateEndComponents()

template<typename ValueType, typename SolutionType>

boost::optional< SparseMdpEndComponentInformation< ValueType > > storm::modelchecker::helper::computeFixedPointSystemUntilProbabilitiesEliminateEndComponents	(	storm::solver::SolveGoal< ValueType, SolutionType > &	goal,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		QualitativeStateSetsUntilProbabilities const &	qualitativeStateSets,
		storm::storage::SparseMatrix< ValueType > &	submatrix,
		std::vector< ValueType > &	b,
		bool	produceScheduler )

Definition at line 644 of file SparseMdpPrctlHelper.cpp.

◆ computeHints()

template<typename ValueType, typename SolutionType>

SparseMdpHintType< SolutionType > storm::modelchecker::helper::computeHints	(	Environment const &	env,
		SemanticSolutionType const &	type,
		ModelCheckerHint const &	hint,
		storm::OptimizationDirection const &	dir,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	maybeStates,
		storm::storage::BitVector const &	phiStates,
		storm::storage::BitVector const &	targetStates,
		bool	produceScheduler,
		boost::optional< storm::storage::BitVector > const &	selectedChoices = boost::none,
		bool	hasUniqueSolution = false )

Definition at line 319 of file SparseMdpPrctlHelper.cpp.

◆ computeOneStepTargetProbabilitiesFromExtendedExplicitRepresentation()

template<typename ValueType>

std::vector< ValueType > storm::modelchecker::helper::computeOneStepTargetProbabilitiesFromExtendedExplicitRepresentation	(	storm::storage::SparseMatrix< ValueType > const &	extendedMatrix,
		storm::storage::BitVector const &	properMaybeStates,
		storm::storage::BitVector const &	targetStates )

Definition at line 489 of file HybridMdpPrctlHelper.cpp.

◆ computeQualitativeStateSetsReachabilityRewards()

template<typename ValueType, typename SolutionType>

QualitativeStateSetsReachabilityRewards storm::modelchecker::helper::computeQualitativeStateSetsReachabilityRewards	(	Environment const &	env,
		storm::solver::SolveGoal< ValueType, SolutionType > const &	goal,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	targetStates,
		std::function< storm::storage::BitVector()> const &	zeroRewardStatesGetter,
		std::function< storm::storage::BitVector()> const &	zeroRewardChoicesGetter )

Definition at line 1163 of file SparseMdpPrctlHelper.cpp.

◆ computeQualitativeStateSetsUntilProbabilities()

template<typename ValueType, typename SolutionType>

QualitativeStateSetsUntilProbabilities storm::modelchecker::helper::computeQualitativeStateSetsUntilProbabilities	(	storm::solver::SolveGoal< ValueType, SolutionType > const &	goal,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	phiStates,
		storm::storage::BitVector const &	psiStates )

Definition at line 534 of file SparseMdpPrctlHelper.cpp.

◆ computeRobustValuesForMaybeStates()

template<typename ValueType, typename SolutionType>

std::vector< SolutionType > storm::modelchecker::helper::computeRobustValuesForMaybeStates	(	Environment const &	env,
		storm::solver::SolveGoal< ValueType, SolutionType > &&	goal,
		storm::storage::SparseMatrix< ValueType > &&	submatrix,
		std::vector< ValueType > const &	b,
		bool	computeReward,
		storm::solver::SolutionBounds< SolutionType > &	solutionBounds )

Definition at line 136 of file SparseDtmcPrctlHelper.cpp.

◆ computeTargetStatesForReachabilityRewardsFromExplicitRepresentation()

template<typename ValueType>

storm::storage::BitVector storm::modelchecker::helper::computeTargetStatesForReachabilityRewardsFromExplicitRepresentation ( storm::storage::SparseMatrix< ValueType > const & transitionMatrix )

Definition at line 454 of file HybridMdpPrctlHelper.cpp.

◆ computeUpperBoundsForExpectedVisitingTimes() [1/2]

template<>

std::vector< storm::RationalFunction > storm::modelchecker::helper::computeUpperBoundsForExpectedVisitingTimes	(	storm::storage::SparseMatrix< storm::RationalFunction > const &	,
		std::vector< storm::RationalFunction > const &	)

Definition at line 640 of file SparseDeterministicInfiniteHorizonHelper.cpp.

◆ computeUpperBoundsForExpectedVisitingTimes() [2/2]

template<typename ValueType>

std::vector< ValueType > storm::modelchecker::helper::computeUpperBoundsForExpectedVisitingTimes	(	storm::storage::SparseMatrix< ValueType > const &	nonBsccMatrix,
		std::vector< ValueType > const &	toBsccProbabilities )

Definition at line 634 of file SparseDeterministicInfiniteHorizonHelper.cpp.

◆ computeUpperRewardBounds() [1/5]

template<typename ValueType, typename SolutionType>

void storm::modelchecker::helper::computeUpperRewardBounds	(	SparseMdpHintType< SolutionType > &	hintInformation,
		storm::OptimizationDirection const &	direction,
		storm::storage::SparseMatrix< ValueType > const &	submatrix,
		std::vector< ValueType > const &	choiceRewards,
		std::vector< ValueType > const &	oneStepTargetProbabilities )

Definition at line 1396 of file SparseMdpPrctlHelper.cpp.

◆ computeUpperRewardBounds() [2/5]

template<>

std::vector< storm::RationalFunction > storm::modelchecker::helper::computeUpperRewardBounds	(	storm::storage::SparseMatrix< storm::RationalFunction > const &	,
		std::vector< storm::RationalFunction > const &	,
		std::vector< storm::RationalFunction > const &	)

Definition at line 601 of file SparseDtmcPrctlHelper.cpp.

◆ computeUpperRewardBounds() [3/5]

template<>

std::vector< storm::RationalFunction > storm::modelchecker::helper::computeUpperRewardBounds	(	storm::storage::SparseMatrix< storm::RationalFunction > const &	transitionMatrix,
		std::vector< storm::RationalFunction > const &	rewards,
		std::vector< storm::RationalFunction > const &	oneStepTargetProbabilities )

inline

Definition at line 270 of file HybridDtmcPrctlHelper.cpp.

◆ computeUpperRewardBounds() [4/5]

template<typename ValueType, typename SolutionType>

std::vector< SolutionType > storm::modelchecker::helper::computeUpperRewardBounds	(	storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		std::vector< ValueType > const &	rewards,
		std::vector< SolutionType > const &	oneStepTargetProbabilities )

Definition at line 589 of file SparseDtmcPrctlHelper.cpp.

◆ computeUpperRewardBounds() [5/5]

template<typename ValueType>

std::vector< ValueType > storm::modelchecker::helper::computeUpperRewardBounds	(	storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		std::vector< ValueType > const &	rewards,
		std::vector< ValueType > const &	oneStepTargetProbabilities )

inline

Definition at line 262 of file HybridDtmcPrctlHelper.cpp.

◆ computeValidInitialSchedulerForReachabilityRewards()

template<typename ValueType>

std::vector< uint64_t > storm::modelchecker::helper::computeValidInitialSchedulerForReachabilityRewards	(	storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::BitVector const &	properMaybeStates,
		storm::storage::BitVector const &	targetStates )

Definition at line 468 of file HybridMdpPrctlHelper.cpp.

◆ computeValidInitialSchedulerForUntilProbabilities()

template<typename ValueType>

std::vector< uint64_t > storm::modelchecker::helper::computeValidInitialSchedulerForUntilProbabilities	(	storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		std::vector< ValueType > const &	b )

Definition at line 57 of file HybridMdpPrctlHelper.cpp.

◆ computeValidSchedulerHint() [1/2]

template<typename ValueType, typename SolutionType = ValueType>

std::vector< uint_fast64_t > storm::modelchecker::helper::computeValidSchedulerHint	(	Environment const &	env,
		SemanticSolutionType const &	type,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	maybeStates,
		storm::storage::BitVector const &	filterStates,
		storm::storage::BitVector const &	targetStates,
		boost::optional< storm::storage::BitVector > const &	selectedChoices )

Definition at line 140 of file SparseMdpPrctlHelper.cpp.

◆ computeValidSchedulerHint() [2/2]

template<storm::dd::DdType DdType, typename ValueType>

storm::dd::Bdd< DdType > storm::modelchecker::helper::computeValidSchedulerHint	(	EquationSystemType const &	type,
		storm::models::symbolic::NondeterministicModel< DdType, ValueType > const &	model,
		storm::dd::Add< DdType, ValueType > const &	transitionMatrix,
		storm::dd::Bdd< DdType > const &	maybeStates,
		storm::dd::Bdd< DdType > const &	targetStates )

Definition at line 30 of file SymbolicMdpPrctlHelper.cpp.

◆ computeValuesForMaybeStates()

template<typename ValueType, typename SolutionType>

MaybeStateResult< SolutionType > storm::modelchecker::helper::computeValuesForMaybeStates	(	Environment const &	env,
		storm::solver::SolveGoal< ValueType, SolutionType > &&	goal,
		storm::storage::SparseMatrix< ValueType > &&	submatrix,
		std::vector< ValueType > const &	b,
		bool	produceScheduler,
		SparseMdpHintType< SolutionType > &	hint )

Definition at line 431 of file SparseMdpPrctlHelper.cpp.

◆ discretizeRewardModel()

template<storm::dd::DdType DdType, class ValueType>

void storm::modelchecker::helper::discretizeRewardModel	(	typename storm::models::symbolic::Model< DdType, ValueType >::RewardModelType &	rewardModel,
		storm::dd::Add< DdType, ValueType > const &	exitRateVector,
		storm::dd::Bdd< DdType > const &	markovianStates )

Definition at line 32 of file HybridMarkovAutomatonCslHelper.cpp.

◆ eliminateEndComponentsAndExtendedStatesUntilProbabilities()

template<typename ValueType>

void storm::modelchecker::helper::eliminateEndComponentsAndExtendedStatesUntilProbabilities	(	std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > &	explicitRepresentation,
		SolverRequirementsData< ValueType > &	solverRequirementsData,
		storm::storage::BitVector const &	targetStates )

Definition at line 108 of file HybridMdpPrctlHelper.cpp.

◆ eliminateEndComponentsAndTargetStatesReachabilityRewards()

template<typename ValueType>

void storm::modelchecker::helper::eliminateEndComponentsAndTargetStatesReachabilityRewards	(	std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > &	explicitRepresentation,
		SolverRequirementsData< ValueType > &	solverRequirementsData,
		storm::storage::BitVector const &	targetStates,
		bool	computeOneStepTargetProbabilities )

Definition at line 496 of file HybridMdpPrctlHelper.cpp.

◆ eliminateExtendedStatesFromExplicitRepresentation()

template<typename ValueType>

void storm::modelchecker::helper::eliminateExtendedStatesFromExplicitRepresentation	(	std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > &	explicitRepresentation,
		boost::optional< std::vector< uint64_t > > &	scheduler,
		storm::storage::BitVector const &	properMaybeStates )

Definition at line 90 of file HybridMdpPrctlHelper.cpp.

◆ expandSolutionAfterEndComponentElimination()

template<typename ValueType>

void storm::modelchecker::helper::expandSolutionAfterEndComponentElimination	(	SolverRequirementsData< ValueType > &	solverRequirementsData,
		std::vector< ValueType > &	x )

Lifts the solution of an equation system in which end components have been eliminated back to the proper maybe states.

Parameters

x	Contains the solution for the system after EC elimination on input and the values for the proper maybe states on output.

Definition at line 49 of file HybridMdpPrctlHelper.cpp.

◆ extendScheduler() [1/2]

template<typename ValueType, typename SolutionType>

void storm::modelchecker::helper::extendScheduler	(	storm::storage::Scheduler< SolutionType > &	scheduler,
		bool	minimize,
		QualitativeStateSetsReachabilityRewards const &	qualitativeStateSets,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	targetStates,
		std::function< storm::storage::BitVector()> const &	zeroRewardChoicesGetter )

Definition at line 1207 of file SparseMdpPrctlHelper.cpp.

◆ extendScheduler() [2/2]

template<typename ValueType, typename SolutionType>

void storm::modelchecker::helper::extendScheduler	(	storm::storage::Scheduler< SolutionType > &	scheduler,
		bool	minimize,
		QualitativeStateSetsUntilProbabilities const &	qualitativeStateSets,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	phiStates,
		storm::storage::BitVector const &	psiStates )

Definition at line 591 of file SparseMdpPrctlHelper.cpp.

◆ extractSchedulerChoices() [1/2]

template<typename SolutionType, bool subChoicesCoverOnlyMaybeStates = true>

void storm::modelchecker::helper::extractSchedulerChoices	(	storm::storage::Scheduler< SolutionType > &	scheduler,
		std::vector< uint64_t > const &	subChoices,
		storm::storage::BitVector const &	maybeStates )

Definition at line 571 of file SparseMdpPrctlHelper.cpp.

◆ extractSchedulerChoices() [2/2]

template<typename ValueType, typename SolutionType>

void storm::modelchecker::helper::extractSchedulerChoices	(	storm::storage::Scheduler< SolutionType > &	scheduler,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		std::vector< uint_fast64_t > const &	subChoices,
		storm::storage::BitVector const &	maybeStates,
		boost::optional< storm::storage::BitVector > const &	selectedChoices )

Definition at line 1227 of file SparseMdpPrctlHelper.cpp.

◆ extractValueAndSchedulerHint()

template<typename ValueType, typename SolutionType>

void storm::modelchecker::helper::extractValueAndSchedulerHint	(	SparseMdpHintType< SolutionType > &	hintStorage,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	maybeStates,
		boost::optional< storm::storage::BitVector > const &	selectedChoices,
		ModelCheckerHint const &	hint,
		bool	skipECWithinMaybeStatesCheck )

Definition at line 260 of file SparseMdpPrctlHelper.cpp.

◆ getQualitativeStateSetsReachabilityRewards()

template<typename ValueType, typename SolutionType>

QualitativeStateSetsReachabilityRewards storm::modelchecker::helper::getQualitativeStateSetsReachabilityRewards	(	Environment const &	env,
		storm::solver::SolveGoal< ValueType, SolutionType > const &	goal,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	targetStates,
		ModelCheckerHint const &	hint,
		std::function< storm::storage::BitVector()> const &	zeroRewardStatesGetter,
		std::function< storm::storage::BitVector()> const &	zeroRewardChoicesGetter )

Definition at line 1194 of file SparseMdpPrctlHelper.cpp.

◆ getQualitativeStateSetsReachabilityRewardsFromHint()

template<typename ValueType>

QualitativeStateSetsReachabilityRewards storm::modelchecker::helper::getQualitativeStateSetsReachabilityRewardsFromHint	(	ModelCheckerHint const &	hint,
		storm::storage::BitVector const &	targetStates )

Definition at line 1139 of file SparseMdpPrctlHelper.cpp.

◆ getQualitativeStateSetsUntilProbabilities()

template<typename ValueType, typename SolutionType>

QualitativeStateSetsUntilProbabilities storm::modelchecker::helper::getQualitativeStateSetsUntilProbabilities	(	storm::solver::SolveGoal< ValueType, SolutionType > const &	goal,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	phiStates,
		storm::storage::BitVector const &	psiStates,
		ModelCheckerHint const &	hint )

Definition at line 558 of file SparseMdpPrctlHelper.cpp.

◆ getQualitativeStateSetsUntilProbabilitiesFromHint()

template<typename ValueType>

QualitativeStateSetsUntilProbabilities storm::modelchecker::helper::getQualitativeStateSetsUntilProbabilitiesFromHint ( ModelCheckerHint const & hint )

Definition at line 510 of file SparseMdpPrctlHelper.cpp.

◆ setInformationFromCheckTaskDeterministic()

template<typename HelperType, typename FormulaType, typename ModelType>

void storm::modelchecker::helper::setInformationFromCheckTaskDeterministic	(	HelperType &	helper,
		storm::modelchecker::CheckTask< FormulaType, typename ModelType::ValueType > const &	checkTask,
		ModelType const &	model )

Forwards relevant information stored in the given CheckTask to the given helper.

Definition at line 39 of file SetInformationFromCheckTask.h.

◆ setInformationFromCheckTaskNondeterministic()

template<typename HelperType, typename FormulaType, typename ModelType>

void storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic	(	HelperType &	helper,
		storm::modelchecker::CheckTask< FormulaType, typename ModelType::ValueType > const &	checkTask,
		ModelType const &	model )

Forwards relevant information stored in the given CheckTask to the given helper.

Definition at line 13 of file SetInformationFromCheckTask.h.

◆ setInformationFromOtherHelperDeterministic()

template<typename TargetHelperType, typename SourceHelperType>

void storm::modelchecker::helper::setInformationFromOtherHelperDeterministic	(	TargetHelperType &	targetHelper,
		SourceHelperType const &	sourceHelperType,
		std::function< typename TargetHelperType::StateSet(typename SourceHelperType::StateSet const &)> const &	stateSetTransformer )

Forwards relevant information stored in another helper to the given helper.

Definition at line 37 of file SetInformationFromOtherHelper.h.

◆ setInformationFromOtherHelperNondeterministic()

template<typename TargetHelperType, typename SourceHelperType>

void storm::modelchecker::helper::setInformationFromOtherHelperNondeterministic	(	TargetHelperType &	targetHelper,
		SourceHelperType const &	sourceHelperType,
		std::function< typename TargetHelperType::StateSet(typename SourceHelperType::StateSet const &)> const &	stateSetTransformer )

Forwards relevant information stored in another helper to the given helper.

Definition at line 13 of file SetInformationFromOtherHelper.h.

◆ setUpperRewardBounds()

template<typename ValueType>

void storm::modelchecker::helper::setUpperRewardBounds	(	storm::solver::MinMaxLinearEquationSolver< ValueType > &	solver,
		storm::OptimizationDirection const &	direction,
		storm::storage::SparseMatrix< ValueType > const &	submatrix,
		std::vector< ValueType > const &	choiceRewards,
		std::vector< ValueType > const &	oneStepTargetProbabilities )

Definition at line 576 of file HybridMdpPrctlHelper.cpp.

◆ setUpProbabilisticStatesSolver()

template<typename ValueType>

std::unique_ptr< storm::solver::MinMaxLinearEquationSolver< ValueType > > storm::modelchecker::helper::setUpProbabilisticStatesSolver	(	storm::Environment &	env,
		OptimizationDirection	dir,
		storm::storage::SparseMatrix< ValueType > const &	transitions )

Definition at line 33 of file SparseMarkovAutomatonCslHelper.cpp.

Namespaces

Classes

Enumerations

Functions

Enumeration Type Documentation

◆ EquationSystemType

◆ SemanticSolutionType

Function Documentation

◆ addSspMatrixChoice()

◆ computeBoundedReachabilityProbabilitiesImca()

◆ computeBoundedUntilProbabilitiesImca()

◆ computeFixedPointSystemReachabilityRewards()

◆ computeFixedPointSystemReachabilityRewardsEliminateEndComponents()

◆ computeFixedPointSystemUntilProbabilities()

◆ computeFixedPointSystemUntilProbabilitiesEliminateEndComponents()

◆ computeHints()

◆ computeOneStepTargetProbabilitiesFromExtendedExplicitRepresentation()

◆ computeQualitativeStateSetsReachabilityRewards()

◆ computeQualitativeStateSetsUntilProbabilities()

◆ computeRobustValuesForMaybeStates()

◆ computeTargetStatesForReachabilityRewardsFromExplicitRepresentation()

◆ computeUpperBoundsForExpectedVisitingTimes() [1/2]

◆ computeUpperBoundsForExpectedVisitingTimes() [2/2]

◆ computeUpperRewardBounds() [1/5]

◆ computeUpperRewardBounds() [2/5]

◆ computeUpperRewardBounds() [3/5]

◆ computeUpperRewardBounds() [4/5]

◆ computeUpperRewardBounds() [5/5]

◆ computeValidInitialSchedulerForReachabilityRewards()

◆ computeValidInitialSchedulerForUntilProbabilities()

◆ computeValidSchedulerHint() [1/2]

◆ computeValidSchedulerHint() [2/2]

◆ computeValuesForMaybeStates()

◆ discretizeRewardModel()

◆ eliminateEndComponentsAndExtendedStatesUntilProbabilities()

◆ eliminateEndComponentsAndTargetStatesReachabilityRewards()

◆ eliminateExtendedStatesFromExplicitRepresentation()

◆ expandSolutionAfterEndComponentElimination()

◆ extendScheduler() [1/2]

◆ extendScheduler() [2/2]

◆ extractSchedulerChoices() [1/2]

◆ extractSchedulerChoices() [2/2]

◆ extractValueAndSchedulerHint()

◆ getQualitativeStateSetsReachabilityRewards()

◆ getQualitativeStateSetsReachabilityRewardsFromHint()

◆ getQualitativeStateSetsUntilProbabilities()

◆ getQualitativeStateSetsUntilProbabilitiesFromHint()

◆ setInformationFromCheckTaskDeterministic()

◆ setInformationFromCheckTaskNondeterministic()

◆ setInformationFromOtherHelperDeterministic()

◆ setInformationFromOtherHelperNondeterministic()

◆ setUpperRewardBounds()

◆ setUpProbabilisticStatesSolver()