#include <CheckTask.h>

Public Member Functions
	CheckTask (FormulaType const &formula, bool onlyInitialStatesRelevant=false)
	Creates a task object with the default options for the given formula.

template<typename NewFormulaType >
CheckTask< NewFormulaType, ValueType >	substituteFormula (NewFormulaType const &newFormula) const
	Copies the check task from the source while replacing the formula with the new one.

void	updateOperatorInformation ()
	If the currently specified formula is an OperatorFormula, this method updates the information that is given in the Operator formula.

CheckTask	negate () const
	Negate the optimization direction and the bound threshold, if those exist.

template<typename NewValueType >
CheckTask< FormulaType, NewValueType >	convertValueType () const
	Copies the check task from the source while replacing the considered ValueType the new one.

FormulaType const &	getFormula () const
	Retrieves the formula from this task.

bool	isOptimizationDirectionSet () const
	Retrieves whether an optimization direction was set.

storm::OptimizationDirection const &	getOptimizationDirection () const
	Retrieves the optimization direction (if set).

void	setOptimizationDirection (storm::OptimizationDirection const &dir)
	Sets the optimization direction.

bool	isPlayerCoalitionSet () const
	Retrieves whether a player coalition was set.

storm::logic::PlayerCoalition const &	getPlayerCoalition () const
	Retrieves the player coalition (if set).

CheckTask< FormulaType, ValueType > &	setPlayerCoalition (storm::logic::PlayerCoalition const &coalition)
	Sets the player coalition.

bool	isRewardModelSet () const
	Retrieves whether a reward model was set.

std::string const &	getRewardModel () const
	Retrieves the reward model over which to perform the checking (if set).

bool	isOnlyInitialStatesRelevantSet () const
	Retrieves whether only the initial states are relevant in the computation.

CheckTask< FormulaType, ValueType > &	setOnlyInitialStatesRelevant (bool value=true)
	Sets whether only initial states are relevant.

bool	isBoundSet () const
	Retrieves whether there is a bound with which the values for the states will be compared.

ValueType	getBoundThreshold () const
	Retrieves the value of the bound (if set).

storm::logic::ComparisonType const &	getBoundComparisonType () const
	Retrieves the comparison type of the bound (if set).

storm::logic::Bound const &	getBound () const
	Retrieves the bound (if set).

boost::optional< storm::logic::Bound > const &	getOptionalBound () const
	Retrieves the bound.

bool	isQualitativeSet () const
	Retrieves whether the computation only needs to be performed qualitatively, because the values will only be compared to 0/1.

void	setQualitative (bool value)
	sets whether the computation only needs to be performed qualitatively, because the values will only be compared to 0/1.

void	setProduceSchedulers (bool produceSchedulers=true)
	Sets whether to produce schedulers (if supported).

bool	isProduceSchedulersSet () const
	Retrieves whether scheduler(s) are to be produced (if supported).

void	setHint (std::shared_ptr< ModelCheckerHint > const &hint)
	sets a hint that might contain information that speeds up the modelchecking process (if supported by the model checker)

ModelCheckerHint const &	getHint () const
	Retrieves a hint that might contain information that speeds up the modelchecking process (if supported by the model checker)

ModelCheckerHint &	getHint ()

	operator CheckTask< storm::logic::Formula, ValueType > () const
	Conversion operator that strips the type of the formula.

bool	getRobustUncertainty () const

void	setRobustUncertainty (bool robust=true)

Friends
template<typename OtherFormulaType , typename OtherValueType >
class	CheckTask

Detailed Description

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>
class storm::modelchecker::CheckTask< FormulaType, ValueType >

Definition at line 30 of file CheckTask.h.

Constructor & Destructor Documentation

◆ CheckTask()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

storm::modelchecker::CheckTask< FormulaType, ValueType >::CheckTask	(	FormulaType const &	formula,
		bool	onlyInitialStatesRelevant = `false`
	)

inline

Creates a task object with the default options for the given formula.

Definition at line 38 of file CheckTask.h.

Member Function Documentation

◆ convertValueType()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

template<typename NewValueType >

CheckTask< FormulaType, NewValueType > storm::modelchecker::CheckTask< FormulaType, ValueType >::convertValueType ( ) const

inline

Copies the check task from the source while replacing the considered ValueType the new one.

In particular, this changes the formula type of the check task object.

Definition at line 131 of file CheckTask.h.

◆ getBound()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

storm::logic::Bound const & storm::modelchecker::CheckTask< FormulaType, ValueType >::getBound ( ) const

inline

Retrieves the bound (if set).

Definition at line 242 of file CheckTask.h.

◆ getBoundComparisonType()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

storm::logic::ComparisonType const & storm::modelchecker::CheckTask< FormulaType, ValueType >::getBoundComparisonType ( ) const

inline

Retrieves the comparison type of the bound (if set).

Definition at line 235 of file CheckTask.h.

◆ getBoundThreshold()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

ValueType storm::modelchecker::CheckTask< FormulaType, ValueType >::getBoundThreshold ( ) const

inline

Retrieves the value of the bound (if set).

Definition at line 226 of file CheckTask.h.

◆ getFormula()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

FormulaType const & storm::modelchecker::CheckTask< FormulaType, ValueType >::getFormula ( ) const

inline

Retrieves the formula from this task.

Definition at line 140 of file CheckTask.h.

◆ getHint() [1/2]

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

ModelCheckerHint & storm::modelchecker::CheckTask< FormulaType, ValueType >::getHint ( )

inline

Definition at line 297 of file CheckTask.h.

◆ getHint() [2/2]

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

ModelCheckerHint const & storm::modelchecker::CheckTask< FormulaType, ValueType >::getHint ( ) const

inline

Retrieves a hint that might contain information that speeds up the modelchecking process (if supported by the model checker)

Definition at line 293 of file CheckTask.h.

◆ getOptimizationDirection()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

storm::OptimizationDirection const & storm::modelchecker::CheckTask< FormulaType, ValueType >::getOptimizationDirection ( ) const

inline

Retrieves the optimization direction (if set).

Definition at line 154 of file CheckTask.h.

◆ getOptionalBound()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

boost::optional< storm::logic::Bound > const & storm::modelchecker::CheckTask< FormulaType, ValueType >::getOptionalBound ( ) const

inline

Retrieves the bound.

Definition at line 249 of file CheckTask.h.

◆ getPlayerCoalition()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

storm::logic::PlayerCoalition const & storm::modelchecker::CheckTask< FormulaType, ValueType >::getPlayerCoalition ( ) const

inline

Retrieves the player coalition (if set).

Definition at line 175 of file CheckTask.h.

◆ getRewardModel()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

std::string const & storm::modelchecker::CheckTask< FormulaType, ValueType >::getRewardModel ( ) const

inline

Retrieves the reward model over which to perform the checking (if set).

Definition at line 197 of file CheckTask.h.

◆ getRobustUncertainty()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

bool storm::modelchecker::CheckTask< FormulaType, ValueType >::getRobustUncertainty ( ) const

inline

Definition at line 308 of file CheckTask.h.

◆ isBoundSet()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

bool storm::modelchecker::CheckTask< FormulaType, ValueType >::isBoundSet ( ) const

inline

Retrieves whether there is a bound with which the values for the states will be compared.

Definition at line 219 of file CheckTask.h.

◆ isOnlyInitialStatesRelevantSet()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

bool storm::modelchecker::CheckTask< FormulaType, ValueType >::isOnlyInitialStatesRelevantSet ( ) const

inline

Retrieves whether only the initial states are relevant in the computation.

Definition at line 204 of file CheckTask.h.

◆ isOptimizationDirectionSet()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

bool storm::modelchecker::CheckTask< FormulaType, ValueType >::isOptimizationDirectionSet ( ) const

inline

Retrieves whether an optimization direction was set.

Definition at line 147 of file CheckTask.h.

◆ isPlayerCoalitionSet()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

bool storm::modelchecker::CheckTask< FormulaType, ValueType >::isPlayerCoalitionSet ( ) const

inline

Retrieves whether a player coalition was set.

Definition at line 168 of file CheckTask.h.

◆ isProduceSchedulersSet()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

bool storm::modelchecker::CheckTask< FormulaType, ValueType >::isProduceSchedulersSet ( ) const

inline

Retrieves whether scheduler(s) are to be produced (if supported).

Definition at line 279 of file CheckTask.h.

◆ isQualitativeSet()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

bool storm::modelchecker::CheckTask< FormulaType, ValueType >::isQualitativeSet ( ) const

inline

Retrieves whether the computation only needs to be performed qualitatively, because the values will only be compared to 0/1.

Definition at line 257 of file CheckTask.h.

◆ isRewardModelSet()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

bool storm::modelchecker::CheckTask< FormulaType, ValueType >::isRewardModelSet ( ) const

inline

Retrieves whether a reward model was set.

Definition at line 190 of file CheckTask.h.

◆ negate()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

CheckTask storm::modelchecker::CheckTask< FormulaType, ValueType >::negate ( ) const

inline

Negate the optimization direction and the bound threshold, if those exist.

Suitable for switching from Pmin[phi] to 1-Pmax[!psi] computations.

Definition at line 110 of file CheckTask.h.

◆ operator CheckTask< storm::logic::Formula, ValueType >()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

storm::modelchecker::CheckTask< FormulaType, ValueType >::operator CheckTask< storm::logic::Formula, ValueType > ( ) const

inline

Conversion operator that strips the type of the formula.

Definition at line 304 of file CheckTask.h.

◆ setHint()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

void storm::modelchecker::CheckTask< FormulaType, ValueType >::setHint ( std::shared_ptr< ModelCheckerHint > const & hint )

inline

sets a hint that might contain information that speeds up the modelchecking process (if supported by the model checker)

Definition at line 286 of file CheckTask.h.

◆ setOnlyInitialStatesRelevant()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

CheckTask< FormulaType, ValueType > & storm::modelchecker::CheckTask< FormulaType, ValueType >::setOnlyInitialStatesRelevant ( bool value = true )

inline

Sets whether only initial states are relevant.

Definition at line 211 of file CheckTask.h.

◆ setOptimizationDirection()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

void storm::modelchecker::CheckTask< FormulaType, ValueType >::setOptimizationDirection ( storm::OptimizationDirection const & dir )

inline

Sets the optimization direction.

Definition at line 161 of file CheckTask.h.

◆ setPlayerCoalition()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

CheckTask< FormulaType, ValueType > & storm::modelchecker::CheckTask< FormulaType, ValueType >::setPlayerCoalition ( storm::logic::PlayerCoalition const & coalition )

inline

Sets the player coalition.

Definition at line 182 of file CheckTask.h.

◆ setProduceSchedulers()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

void storm::modelchecker::CheckTask< FormulaType, ValueType >::setProduceSchedulers ( bool produceSchedulers = true )

inline

Sets whether to produce schedulers (if supported).

Definition at line 272 of file CheckTask.h.

◆ setQualitative()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

void storm::modelchecker::CheckTask< FormulaType, ValueType >::setQualitative ( bool value )

inline

sets whether the computation only needs to be performed qualitatively, because the values will only be compared to 0/1.

Definition at line 265 of file CheckTask.h.

◆ setRobustUncertainty()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

void storm::modelchecker::CheckTask< FormulaType, ValueType >::setRobustUncertainty ( bool robust = true )

inline

Definition at line 312 of file CheckTask.h.

◆ substituteFormula()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

template<typename NewFormulaType >

CheckTask< NewFormulaType, ValueType > storm::modelchecker::CheckTask< FormulaType, ValueType >::substituteFormula ( NewFormulaType const & newFormula ) const

inline

Copies the check task from the source while replacing the formula with the new one.

In particular, this changes the formula type of the check task object.

Definition at line 52 of file CheckTask.h.

◆ updateOperatorInformation()

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

void storm::modelchecker::CheckTask< FormulaType, ValueType >::updateOperatorInformation ( )

inline

If the currently specified formula is an OperatorFormula, this method updates the information that is given in the Operator formula.

Calling this method has no effect if the provided formula is not an operator formula.

Definition at line 64 of file CheckTask.h.

Friends And Related Symbol Documentation

◆ CheckTask

template<typename FormulaType = storm::logic::Formula, typename ValueType = double>

template<typename OtherFormulaType , typename OtherValueType >

friend class CheckTask

friend

Definition at line 33 of file CheckTask.h.

The documentation for this class was generated from the following files:

src/storm-pomdp/builder/BeliefMdpExplorer.h
src/storm/modelchecker/CheckTask.h

Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ CheckTask()

Member Function Documentation

◆ convertValueType()

◆ getBound()

◆ getBoundComparisonType()

◆ getBoundThreshold()

◆ getFormula()

◆ getHint() [1/2]

◆ getHint() [2/2]

◆ getOptimizationDirection()

◆ getOptionalBound()

◆ getPlayerCoalition()

◆ getRewardModel()

◆ getRobustUncertainty()

◆ isBoundSet()

◆ isOnlyInitialStatesRelevantSet()

◆ isOptimizationDirectionSet()

◆ isPlayerCoalitionSet()

◆ isProduceSchedulersSet()

◆ isQualitativeSet()

◆ isRewardModelSet()

◆ negate()

◆ operator CheckTask< storm::logic::Formula, ValueType >()

◆ setHint()

◆ setOnlyInitialStatesRelevant()

◆ setOptimizationDirection()

◆ setPlayerCoalition()

◆ setProduceSchedulers()

◆ setQualitative()

◆ setRobustUncertainty()

◆ substituteFormula()

◆ updateOperatorInformation()

Friends And Related Symbol Documentation

◆ CheckTask