Namespaces
namespace	internal

namespace	lexicographic

namespace	rewardbounded

Classes
class	BaierUpperRewardBoundsComputer

class	DsMpiDtmcPriorityLess

class	DsMpiDtmcUpperRewardBoundsComputer

class	DsMpiMdpPriorityLess

class	DsMpiMdpUpperRewardBoundsComputer

class	HybridCtmcCslHelper

class	HybridDtmcPrctlHelper

class	HybridInfiniteHorizonHelper
	Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. More...

class	HybridMarkovAutomatonCslHelper

class	HybridMdpPrctlHelper

struct	MaybeStateResult

struct	MDPSparseModelCheckingHelperReturnType

class	ModelCheckerHelper
	Helper class for solving a model checking query. More...

struct	QualitativeStateSetsReachabilityRewards

struct	QualitativeStateSetsUntilProbabilities

class	SingleValueModelCheckerHelper
	Helper for model checking queries where we are interested in (optimizing) a single value per state. More...

struct	SolverRequirementsData

class	SparseCtmcCslHelper

class	SparseDeterministicInfiniteHorizonHelper
	Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. More...

class	SparseDeterministicStepBoundedHorizonHelper

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	SparseDtmcPrctlHelper

class	SparseInfiniteHorizonHelper
	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	SparseMarkovAutomatonCslHelper

class	SparseMdpEndComponentInformation

struct	SparseMdpHintType

class	SparseMdpPrctlHelper

class	SparseNondeterministicInfiniteHorizonHelper
	Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. More...

class	SparseNondeterministicStepBoundedHorizonHelper

class	SymbolicDtmcPrctlHelper

class	SymbolicMdpPrctlHelper

class	UnifPlusHelper

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<>
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 272 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 488 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 612 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 1176 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 1206 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 619 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 651 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 343 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 1084 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 540 of file SparseMdpPrctlHelper.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 649 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 643 of file SparseDeterministicInfiniteHorizonHelper.cpp.

◆ computeUpperRewardBounds() [1/4]

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 1291 of file SparseMdpPrctlHelper.cpp.

◆ computeUpperRewardBounds() [2/4]

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 433 of file SparseDtmcPrctlHelper.cpp.

◆ computeUpperRewardBounds() [3/4]

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 278 of file HybridDtmcPrctlHelper.cpp.

◆ computeUpperRewardBounds() [4/4]

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 270 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 166 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 453 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 1130 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 597 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 577 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 1151 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 286 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 1115 of file SparseMdpPrctlHelper.cpp.

◆ getQualitativeStateSetsReachabilityRewardsFromHint()

template<typename ValueType >

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

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

◆ getQualitativeStateSetsUntilProbabilitiesFromHint()

template<typename ValueType >

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

Definition at line 517 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()

◆ computeTargetStatesForReachabilityRewardsFromExplicitRepresentation()

◆ computeUpperBoundsForExpectedVisitingTimes() [1/2]

◆ computeUpperBoundsForExpectedVisitingTimes() [2/2]

◆ computeUpperRewardBounds() [1/4]

◆ computeUpperRewardBounds() [2/4]

◆ computeUpperRewardBounds() [3/4]

◆ computeUpperRewardBounds() [4/4]

◆ 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()