#include <DiscountingHelper.h>

Inheritance diagram for storm::modelchecker::helper::DiscountingHelper< ValueType, TrivialRowGrouping >:

[legend]

Collaboration diagram for storm::modelchecker::helper::DiscountingHelper< ValueType, TrivialRowGrouping >:

[legend]

Public Member Functions
	DiscountingHelper (storm::storage::SparseMatrix< ValueType > const &A, ValueType discountFactor)

	DiscountingHelper (storm::storage::SparseMatrix< ValueType > const &A, ValueType discountFactor, bool trackScheduler)

bool	solveWithDiscountedValueIteration (Environment const &env, std::optional< OptimizationDirection > dir, std::vector< ValueType > &x, std::vector< ValueType > const &b) const

storm::storage::Scheduler< ValueType >	computeScheduler () const
	Retrieves the generated scheduler.

bool	hasScheduler () const
	Retrieves whether the solver generated a scheduler.

void	setTrackScheduler (bool trackScheduler)

bool	isTrackSchedulerSet () const

Public Member Functions inherited from storm::modelchecker::helper::SingleValueModelCheckerHelper< ValueType, storm::models::ModelRepresentation::Sparse >
	SingleValueModelCheckerHelper ()

void	setOptimizationDirection (storm::solver::OptimizationDirection const &direction)
	Sets the optimization direction, i.e., whether we want to minimize or maximize the value for each state Has no effect for models without nondeterminism.

void	clearOptimizationDirection ()
	Clears the optimization direction if it was set before.

bool	isOptimizationDirectionSet () const

storm::solver::OptimizationDirection const &	getOptimizationDirection () const

bool	minimize () const

bool	maximize () const

boost::optional< storm::solver::OptimizationDirection >	getOptionalOptimizationDirection () const

void	setValueThreshold (storm::logic::ComparisonType const &comparisonType, ValueType const &thresholdValue)
	Sets a goal threshold for the value at each state.

void	clearValueThreshold ()
	Clears the valueThreshold if it was set before.

bool	isValueThresholdSet () const

storm::logic::ComparisonType const &	getValueThresholdComparisonType () const

ValueType const &	getValueThresholdValue () const

void	setProduceScheduler (bool value)
	Sets whether an optimal scheduler shall be constructed during the computation.

bool	isProduceSchedulerSet () const

void	setQualitative (bool value)
	Sets whether the property needs to be checked qualitatively.

bool	isQualitativeSet () const

Public Member Functions inherited from storm::modelchecker::helper::ModelCheckerHelper< ValueType, ModelRepresentation >
	ModelCheckerHelper ()=default

virtual	~ModelCheckerHelper ()=default

void	setRelevantStates (StateSet const &relevantStates)
	Sets relevant states.

void	clearRelevantStates ()
	Clears the relevant states.

bool	hasRelevantStates () const

boost::optional< StateSet > const &	getOptionalRelevantStates () const

StateSet const &	getRelevantStates () const

Additional Inherited Members
Public Types inherited from storm::modelchecker::helper::ModelCheckerHelper< ValueType, ModelRepresentation >
typedef ValueType	ValueType

using	StateSet = typename std::conditional< ModelRepresentation==storm::models::ModelRepresentation::Sparse, storm::storage::BitVector, storm::dd::Bdd< storm::models::GetDdType< ModelRepresentation >::ddType > >::type
	Identifies a subset of the model states.

Detailed Description

template<typename ValueType, bool TrivialRowGrouping = false>
class storm::modelchecker::helper::DiscountingHelper< ValueType, TrivialRowGrouping >

Definition at line 13 of file DiscountingHelper.h.