storm::modelchecker::helper::rewardbounded Namespace Reference

Classes
class	CostLimit
class	CostLimitClosure
struct	Dimension
class	EpochManager
struct	EpochModel
class	MemoryStateManager
class	MultiDimensionalRewardUnfolding
class	ProductModel
class	QuantileHelper

Typedefs
typedef std::vector< CostLimit >	CostLimits

Enumerations
enum class	DimensionBoundType { Unbounded , UpperBound , LowerBound , LowerBoundInfinity }
enum class	BoundTransformation { None , GreaterZero , GreaterEqualZero , LessEqualZero }

Functions
template<typename ValueType >
std::vector< ValueType >	analyzeTrivialDtmcEpochModel (EpochModel< ValueType, true > &epochModel)
template<typename ValueType >
std::vector< ValueType >	analyzeNonTrivialDtmcEpochModel (Environment const &env, EpochModel< ValueType, true > &epochModel, std::vector< ValueType > &x, std::vector< ValueType > &b, std::unique_ptr< storm::solver::LinearEquationSolver< ValueType > > &linEqSolver, boost::optional< ValueType > const &lowerBound, boost::optional< ValueType > const &upperBound)
template<typename ValueType >
std::vector< ValueType >	analyzeTrivialMdpEpochModel (OptimizationDirection dir, EpochModel< ValueType, true > &epochModel)
template<typename ValueType >
std::vector< ValueType >	analyzeNonTrivialMdpEpochModel (Environment const &env, OptimizationDirection dir, EpochModel< ValueType, true > &epochModel, std::vector< ValueType > &x, std::vector< ValueType > &b, std::unique_ptr< storm::solver::MinMaxLinearEquationSolver< ValueType > > &minMaxSolver, boost::optional< ValueType > const &lowerBound, boost::optional< ValueType > const &upperBound)
std::shared_ptr< storm::logic::ProbabilityOperatorFormula >	transformBoundedUntilOperator (storm::logic::ProbabilityOperatorFormula const &boundedUntilOperator, std::vector< BoundTransformation > const &transformations, bool complementQuery=false)
void	increasePrecision (storm::Environment &env)
	Increases the precision of solver results.
template<typename ValueType >
std::pair< ValueType, ValueType >	getLowerUpperBound (storm::Environment const &env, ValueType const &factor, ValueType const &value, bool minMax=true)
	Computes a lower / upper bound on the actual result of a sound minmax or linear equation solver.
bool	getNextCandidateCostLimit (CostLimit const &candidateCostLimitSum, CostLimits &current)
bool	translateEpochToCostLimits (EpochManager::Epoch const &epoch, EpochManager::Epoch const &startEpoch, storm::storage::BitVector const &consideredDimensions, storm::storage::BitVector const &lowerBoundedDimensions, EpochManager const &epochManager, CostLimits &epochAsCostLimits)

Typedef Documentation

CostLimits

typedef std::vector<CostLimit> storm::modelchecker::helper::rewardbounded::CostLimits

Definition at line 27 of file CostLimitClosure.h.

Enumeration Type Documentation

BoundTransformation

enum class storm::modelchecker::helper::rewardbounded::BoundTransformation

strong

Enumerator
None
GreaterZero
GreaterEqualZero
LessEqualZero

Definition at line 85 of file QuantileHelper.cpp.

DimensionBoundType

enum class storm::modelchecker::helper::rewardbounded::DimensionBoundType

strong

Enumerator
Unbounded
UpperBound
LowerBound
LowerBoundInfinity

Definition at line 13 of file Dimension.h.

Function Documentation

analyzeNonTrivialDtmcEpochModel()

template<typename ValueType >

std::vector< ValueType > storm::modelchecker::helper::rewardbounded::analyzeNonTrivialDtmcEpochModel	(	Environment const &	env,
		EpochModel< ValueType, true > &	epochModel,
		std::vector< ValueType > &	x,
		std::vector< ValueType > &	b,
		std::unique_ptr< storm::solver::LinearEquationSolver< ValueType > > &	linEqSolver,
		boost::optional< ValueType > const &	lowerBound,
		boost::optional< ValueType > const &	upperBound
	)

Definition at line 45 of file EpochModel.cpp.

analyzeNonTrivialMdpEpochModel()

template<typename ValueType >

std::vector< ValueType > storm::modelchecker::helper::rewardbounded::analyzeNonTrivialMdpEpochModel	(	Environment const &	env,
		OptimizationDirection	dir,
		EpochModel< ValueType, true > &	epochModel,
		std::vector< ValueType > &	x,
		std::vector< ValueType > &	b,
		std::unique_ptr< storm::solver::MinMaxLinearEquationSolver< ValueType > > &	minMaxSolver,
		boost::optional< ValueType > const &	lowerBound,
		boost::optional< ValueType > const &	upperBound
	)

Definition at line 155 of file EpochModel.cpp.

analyzeTrivialDtmcEpochModel()

template<typename ValueType >

std::vector< ValueType > storm::modelchecker::helper::rewardbounded::analyzeTrivialDtmcEpochModel

(

EpochModel< ValueType, true > &

epochModel

)

Definition at line 17 of file EpochModel.cpp.

analyzeTrivialMdpEpochModel()

template<typename ValueType >

std::vector< ValueType > storm::modelchecker::helper::rewardbounded::analyzeTrivialMdpEpochModel	(	OptimizationDirection	dir,
		EpochModel< ValueType, true > &	epochModel
	)

Definition at line 105 of file EpochModel.cpp.

getLowerUpperBound()

template<typename ValueType >

std::pair< ValueType, ValueType > storm::modelchecker::helper::rewardbounded::getLowerUpperBound	(	storm::Environment const &	env,
		ValueType const &	factor,
		ValueType const &	value,
		bool	minMax = true
	)

Computes a lower / upper bound on the actual result of a sound minmax or linear equation solver.

Definition at line 163 of file QuantileHelper.cpp.

getNextCandidateCostLimit()

bool storm::modelchecker::helper::rewardbounded::getNextCandidateCostLimit	(	CostLimit const &	candidateCostLimitSum,
		CostLimits &	current
	)

Definition at line 338 of file QuantileHelper.cpp.

increasePrecision()

void storm::modelchecker::helper::rewardbounded::increasePrecision

(

storm::Environment &

env

)

Increases the precision of solver results.

Definition at line 150 of file QuantileHelper.cpp.

transformBoundedUntilOperator()

std::shared_ptr< storm::logic::ProbabilityOperatorFormula > storm::modelchecker::helper::rewardbounded::transformBoundedUntilOperator	(	storm::logic::ProbabilityOperatorFormula const &	boundedUntilOperator,
		std::vector< BoundTransformation > const &	transformations,
		bool	complementQuery = false
	)

Definition at line 86 of file QuantileHelper.cpp.

translateEpochToCostLimits()

bool storm::modelchecker::helper::rewardbounded::translateEpochToCostLimits	(	EpochManager::Epoch const &	epoch,
		EpochManager::Epoch const &	startEpoch,
		storm::storage::BitVector const &	consideredDimensions,
		storm::storage::BitVector const &	lowerBoundedDimensions,
		EpochManager const &	epochManager,
		CostLimits &	epochAsCostLimits
	)

Definition at line 361 of file QuantileHelper.cpp.