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
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, 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>
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)
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)
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, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, 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 (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 (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, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, 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 507 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, double > const &	boundsPair )

Definition at line 631 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 1213 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 1243 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 606 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 638 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 )

Definition at line 323 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 478 of file HybridMdpPrctlHelper.cpp.

◆ computeQualitativeStateSetsReachabilityRewards()

template<typename ValueType, typename SolutionType>

QualitativeStateSetsReachabilityRewards storm::modelchecker::helper::computeQualitativeStateSetsReachabilityRewards	(	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 1121 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 527 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 )

Definition at line 140 of file SparseDtmcPrctlHelper.cpp.

◆ computeTargetStatesForReachabilityRewardsFromExplicitRepresentation()

template<typename ValueType>

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

Definition at line 443 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 1328 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 574 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 562 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 457 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 44 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 146 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 433 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 95 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 485 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 77 of file HybridMdpPrctlHelper.cpp.

◆ extendScheduler() [1/2]

template<typename ValueType, typename SolutionType>

void storm::modelchecker::helper::extendScheduler	(	storm::storage::Scheduler< SolutionType > &	scheduler,
		storm::solver::SolveGoal< ValueType, SolutionType > const &	goal,
		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 1167 of file SparseMdpPrctlHelper.cpp.

◆ extendScheduler() [2/2]

template<typename ValueType, typename SolutionType>

void storm::modelchecker::helper::extendScheduler	(	storm::storage::Scheduler< SolutionType > &	scheduler,
		storm::solver::SolveGoal< ValueType, SolutionType > const &	goal,
		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 584 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 564 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 1188 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 266 of file SparseMdpPrctlHelper.cpp.

◆ getQualitativeStateSetsReachabilityRewards()

template<typename ValueType, typename SolutionType>

QualitativeStateSetsReachabilityRewards storm::modelchecker::helper::getQualitativeStateSetsReachabilityRewards	(	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 1152 of file SparseMdpPrctlHelper.cpp.

◆ getQualitativeStateSetsReachabilityRewardsFromHint()

template<typename ValueType>

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

Definition at line 1098 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 551 of file SparseMdpPrctlHelper.cpp.

◆ getQualitativeStateSetsUntilProbabilitiesFromHint()

template<typename ValueType>

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

Definition at line 504 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 565 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 32 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()

◆ extendScheduler() [1/2]

◆ extendScheduler() [2/2]

◆ extractSchedulerChoices() [1/2]

◆ extractSchedulerChoices() [2/2]

◆ extractValueAndSchedulerHint()

◆ getQualitativeStateSetsReachabilityRewards()

◆ getQualitativeStateSetsReachabilityRewardsFromHint()

◆ getQualitativeStateSetsUntilProbabilities()

◆ getQualitativeStateSetsUntilProbabilitiesFromHint()

◆ setInformationFromCheckTaskDeterministic()

◆ setInformationFromCheckTaskNondeterministic()

◆ setInformationFromOtherHelperDeterministic()

◆ setInformationFromOtherHelperNondeterministic()

◆ setUpperRewardBounds()

◆ setUpProbabilisticStatesSolver()