#include <CheckTask.h>

Public Member Functions
	CheckTask (FormulaType const &formula, bool onlyInitialStatesRelevant=false, UncertaintyResolutionMode=UncertaintyResolutionMode::Unset)
	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 ()

UncertaintyResolutionMode	getUncertaintyResolutionMode () const
	Retrieves the mode which decides how the uncertainty will be resolved.

void	setUncertaintyResolutionMode (UncertaintyResolutionMode uncertaintyResolutionMode)
	Sets the mode which decides how the uncertainty will be resolved.

bool	isUncertaintyResolutionModeSet () const
	Returns whether the mode, which decides how the uncertainty will be resolved, is set.

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

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 31 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`,
		UncertaintyResolutionMode	= `UncertaintyResolutionMode::Unset`
	)

inline

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

Definition at line 39 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 133 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 244 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 237 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 228 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 142 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 299 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 295 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 156 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 251 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 177 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 199 of file CheckTask.h.

◆ getUncertaintyResolutionMode()

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

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

inline

Retrieves the mode which decides how the uncertainty will be resolved.

Definition at line 306 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 221 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 206 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 149 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 170 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 281 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 259 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 192 of file CheckTask.h.

◆ isUncertaintyResolutionModeSet()

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

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

inline

Returns whether the mode, which decides how the uncertainty will be resolved, is set.

Definition at line 320 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 112 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 327 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 288 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 213 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 163 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 184 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 274 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 267 of file CheckTask.h.

◆ setUncertaintyResolutionMode()

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

void storm::modelchecker::CheckTask< FormulaType, ValueType >::setUncertaintyResolutionMode ( UncertaintyResolutionMode uncertaintyResolutionMode )

inline

Sets the mode which decides how the uncertainty will be resolved.

Definition at line 313 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 54 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 66 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 34 of file CheckTask.h.

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

src/storm-pars/transformer/BigStep.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()

◆ getUncertaintyResolutionMode()

◆ isBoundSet()

◆ isOnlyInitialStatesRelevantSet()

◆ isOptimizationDirectionSet()

◆ isPlayerCoalitionSet()

◆ isProduceSchedulersSet()

◆ isQualitativeSet()

◆ isRewardModelSet()

◆ isUncertaintyResolutionModeSet()

◆ negate()

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

◆ setHint()

◆ setOnlyInitialStatesRelevant()

◆ setOptimizationDirection()

◆ setPlayerCoalition()

◆ setProduceSchedulers()

◆ setQualitative()

◆ setUncertaintyResolutionMode()

◆ substituteFormula()

◆ updateOperatorInformation()

Friends And Related Symbol Documentation

◆ CheckTask