#include <BuilderOptions.h>

Public Member Functions
	BuilderOptions (bool buildAllRewardModels=false, bool buildAllLabels=false)
	Creates an object representing the default options.

	BuilderOptions (storm::logic::Formula const &formula, storm::storage::SymbolicModelDescription const &modelDescription=storm::storage::SymbolicModelDescription())
	Creates an object representing the suggested building options assuming that the given formula is the only one to check.

	BuilderOptions (std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::storage::SymbolicModelDescription const &modelDescription=storm::storage::SymbolicModelDescription())
	Creates an object representing the suggested building options assuming that the given formulas are the only ones to check.

void	preserveFormula (storm::logic::Formula const &formula, storm::storage::SymbolicModelDescription const &modelDescription=storm::storage::SymbolicModelDescription())
	Changes the options in a way that ensures that the given formula can be checked on the model once it has been built.

void	setTerminalStatesFromFormula (storm::logic::Formula const &formula)
	Analyzes the given formula and sets an expression for the states states of the model that can be treated as terminal states.

std::set< std::string > const &	getRewardModelNames () const
	Which reward models are built.

std::set< std::string > const &	getLabelNames () const
	Which labels are built.

std::vector< std::pair< std::string, storm::expressions::Expression > > const &	getExpressionLabels () const
	Which expression labels are built.

std::vector< std::pair< LabelOrExpression, bool > > const &	getTerminalStates () const

bool	hasTerminalStates () const

void	clearTerminalStates ()

bool	isApplyMaximalProgressAssumptionSet () const

bool	isBuildChoiceLabelsSet () const

bool	isBuildStateValuationsSet () const

bool	isBuildObservationValuationsSet () const

bool	isBuildChoiceOriginsSet () const

bool	isBuildAllRewardModelsSet () const

bool	isBuildAllLabelsSet () const

bool	isExplorationChecksSet () const

bool	isInferObservationsFromActionsSet () const

bool	isShowProgressSet () const

bool	isScaleAndLiftTransitionRewardsSet () const

bool	isAddOutOfBoundsStateSet () const

uint64_t	getReservedBitsForUnboundedVariables () const

bool	isAddOverlappingGuardLabelSet () const

uint64_t	getShowProgressDelay () const

storm::RationalNumber const &	getStochasticTolerance () const
	Some distributions may not sum to one.

BuilderOptions &	setBuildAllRewardModels (bool newValue=true)
	Should all reward models be built? If not set, only required reward models are build.

BuilderOptions &	addRewardModel (std::string const &rewardModelName)
	Add an additional reward model to build.

BuilderOptions &	setBuildAllLabels (bool newValue=true)
	Should all reward models be built? If not set, only required reward models are build.

BuilderOptions &	addLabel (storm::expressions::Expression const &expression)

BuilderOptions &	addLabel (std::string const &labelName)

BuilderOptions &	addTerminalExpression (storm::expressions::Expression const &expression, bool value)

BuilderOptions &	addTerminalLabel (std::string const &label, bool value)

BuilderOptions &	setApplyMaximalProgressAssumption (bool newValue=true)
	Should the maximal progress assumption be applied when building a Markov Automaton?

BuilderOptions &	setBuildChoiceLabels (bool newValue=true)
	Should the choice labels be built?

BuilderOptions &	setBuildStateValuations (bool newValue=true)
	Should the state valuation mapping be built?

BuilderOptions &	setBuildObservationValuations (bool newValue=true)
	Should a observation valuation mapping be built?

BuilderOptions &	setBuildChoiceOrigins (bool newValue=true)
	Should the origins the different choices be built?

BuilderOptions &	setExplorationChecks (bool newValue=true)
	Should extra checks be performed during exploration.

BuilderOptions &	setInferObservationsFromActions (bool newValue=true)

BuilderOptions &	setScaleAndLiftTransitionRewards (bool newValue=true)
	Should extra checks be performed during exploration.

BuilderOptions &	setAddOutOfBoundsState (bool newValue=true)
	Should a state for out of bounds be constructed.

BuilderOptions &	setAddOverlappingGuardsLabel (bool newValue=true)
	Should a state be labelled for overlapping guards.

BuilderOptions &	setReservedBitsForUnboundedVariables (uint64_t value)
	Sets the number of bits that will be reserved for unbounded integer variables.

BuilderOptions &	substituteExpressions (std::function< storm::expressions::Expression(storm::expressions::Expression const &)> const &substitutionFunction)
	Substitutes all expressions occurring in these options.

Detailed Description

Definition at line 45 of file BuilderOptions.h.

Constructor & Destructor Documentation

◆ BuilderOptions() [1/3]

storm::builder::BuilderOptions::BuilderOptions	(	bool	buildAllRewardModels = `false`,
		bool	buildAllLabels = `false`
	)

Creates an object representing the default options.

Definition at line 42 of file BuilderOptions.cpp.

◆ BuilderOptions() [2/3]

storm::builder::BuilderOptions::BuilderOptions	(	storm::logic::Formula const &	formula,
		storm::storage::SymbolicModelDescription const &	modelDescription = `storm::storage::SymbolicModelDescription()`
	)

Creates an object representing the suggested building options assuming that the given formula is the only one to check.

Additional formulas may be preserved by calling preserveFormula.

Parameters

formula The formula based on which to choose the building options.

Definition at line 63 of file BuilderOptions.cpp.

◆ BuilderOptions() [3/3]

storm::builder::BuilderOptions::BuilderOptions	(	std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		storm::storage::SymbolicModelDescription const &	modelDescription = `storm::storage::SymbolicModelDescription()`
	)

Creates an object representing the suggested building options assuming that the given formulas are the only ones to check.

Additional formulas may be preserved by calling preserveFormula.

Parameters

formula Thes formula based on which to choose the building options.

Definition at line 68 of file BuilderOptions.cpp.

Member Function Documentation

◆ addLabel() [1/2]

BuilderOptions & storm::builder::BuilderOptions::addLabel ( std::string const & labelName )

Definition at line 240 of file BuilderOptions.cpp.

◆ addLabel() [2/2]

BuilderOptions & storm::builder::BuilderOptions::addLabel ( storm::expressions::Expression const & expression )

Definition at line 233 of file BuilderOptions.cpp.

◆ addRewardModel()

BuilderOptions & storm::builder::BuilderOptions::addRewardModel ( std::string const & rewardModelName )

Add an additional reward model to build.

Parameters

newValue The name of the extra reward model

Returns: this

Definition at line 222 of file BuilderOptions.cpp.

◆ addTerminalExpression()

BuilderOptions & storm::builder::BuilderOptions::addTerminalExpression	(	storm::expressions::Expression const &	expression,
		bool	value
	)

Definition at line 246 of file BuilderOptions.cpp.

◆ addTerminalLabel()

BuilderOptions & storm::builder::BuilderOptions::addTerminalLabel	(	std::string const &	label,
		bool	value
	)

Definition at line 251 of file BuilderOptions.cpp.

◆ clearTerminalStates()

void storm::builder::BuilderOptions::clearTerminalStates ( )

Definition at line 144 of file BuilderOptions.cpp.

◆ getExpressionLabels()

std::vector< std::pair< std::string, storm::expressions::Expression > > const & storm::builder::BuilderOptions::getExpressionLabels ( ) const

Which expression labels are built.

Returns

Definition at line 132 of file BuilderOptions.cpp.

◆ getLabelNames()

std::set< std::string > const & storm::builder::BuilderOptions::getLabelNames ( ) const

Which labels are built.

Returns

Definition at line 128 of file BuilderOptions.cpp.

◆ getReservedBitsForUnboundedVariables()

uint64_t storm::builder::BuilderOptions::getReservedBitsForUnboundedVariables ( ) const

Definition at line 188 of file BuilderOptions.cpp.

◆ getRewardModelNames()

std::set< std::string > const & storm::builder::BuilderOptions::getRewardModelNames ( ) const

Which reward models are built.

Returns

Definition at line 124 of file BuilderOptions.cpp.

◆ getShowProgressDelay()

uint64_t storm::builder::BuilderOptions::getShowProgressDelay ( ) const

Definition at line 209 of file BuilderOptions.cpp.

◆ getStochasticTolerance()

storm::RationalNumber const & storm::builder::BuilderOptions::getStochasticTolerance ( ) const

Some distributions may not sum to one.

This tolerance allows handling this case.

Returns: The tolerance

Definition at line 213 of file BuilderOptions.cpp.

◆ getTerminalStates()

std::vector< std::pair< LabelOrExpression, bool > > const & storm::builder::BuilderOptions::getTerminalStates ( ) const

Definition at line 136 of file BuilderOptions.cpp.

◆ hasTerminalStates()

bool storm::builder::BuilderOptions::hasTerminalStates ( ) const

Definition at line 140 of file BuilderOptions.cpp.

◆ isAddOutOfBoundsStateSet()

bool storm::builder::BuilderOptions::isAddOutOfBoundsStateSet ( ) const

Definition at line 184 of file BuilderOptions.cpp.

◆ isAddOverlappingGuardLabelSet()

bool storm::builder::BuilderOptions::isAddOverlappingGuardLabelSet ( ) const

Definition at line 192 of file BuilderOptions.cpp.

◆ isApplyMaximalProgressAssumptionSet()

bool storm::builder::BuilderOptions::isApplyMaximalProgressAssumptionSet ( ) const

Definition at line 148 of file BuilderOptions.cpp.

◆ isBuildAllLabelsSet()

bool storm::builder::BuilderOptions::isBuildAllLabelsSet ( ) const

Definition at line 172 of file BuilderOptions.cpp.

◆ isBuildAllRewardModelsSet()

bool storm::builder::BuilderOptions::isBuildAllRewardModelsSet ( ) const

Definition at line 168 of file BuilderOptions.cpp.

◆ isBuildChoiceLabelsSet()

bool storm::builder::BuilderOptions::isBuildChoiceLabelsSet ( ) const

Definition at line 152 of file BuilderOptions.cpp.

◆ isBuildChoiceOriginsSet()

bool storm::builder::BuilderOptions::isBuildChoiceOriginsSet ( ) const

Definition at line 164 of file BuilderOptions.cpp.

◆ isBuildObservationValuationsSet()

bool storm::builder::BuilderOptions::isBuildObservationValuationsSet ( ) const

Definition at line 160 of file BuilderOptions.cpp.

◆ isBuildStateValuationsSet()

bool storm::builder::BuilderOptions::isBuildStateValuationsSet ( ) const

Definition at line 156 of file BuilderOptions.cpp.

◆ isExplorationChecksSet()

bool storm::builder::BuilderOptions::isExplorationChecksSet ( ) const

Definition at line 201 of file BuilderOptions.cpp.

◆ isInferObservationsFromActionsSet()

bool storm::builder::BuilderOptions::isInferObservationsFromActionsSet ( ) const

Definition at line 176 of file BuilderOptions.cpp.

◆ isScaleAndLiftTransitionRewardsSet()

bool storm::builder::BuilderOptions::isScaleAndLiftTransitionRewardsSet ( ) const

Definition at line 180 of file BuilderOptions.cpp.

◆ isShowProgressSet()

bool storm::builder::BuilderOptions::isShowProgressSet ( ) const

Definition at line 205 of file BuilderOptions.cpp.

◆ preserveFormula()

void storm::builder::BuilderOptions::preserveFormula	(	storm::logic::Formula const &	formula,
		storm::storage::SymbolicModelDescription const &	modelDescription = `storm::storage::SymbolicModelDescription()`
	)

Changes the options in a way that ensures that the given formula can be checked on the model once it has been built.

Parameters

formula The formula that is to be ''preserved''.

Definition at line 90 of file BuilderOptions.cpp.

◆ setAddOutOfBoundsState()

BuilderOptions & storm::builder::BuilderOptions::setAddOutOfBoundsState ( bool newValue = true )

Should a state for out of bounds be constructed.

Parameters

newValue The new value (default true)

Returns: this

Definition at line 286 of file BuilderOptions.cpp.

◆ setAddOverlappingGuardsLabel()

BuilderOptions & storm::builder::BuilderOptions::setAddOverlappingGuardsLabel ( bool newValue = true )

Should a state be labelled for overlapping guards.

Parameters

newValue the new value (default true)

Definition at line 296 of file BuilderOptions.cpp.

◆ setApplyMaximalProgressAssumption()

BuilderOptions & storm::builder::BuilderOptions::setApplyMaximalProgressAssumption ( bool newValue = true )

Should the maximal progress assumption be applied when building a Markov Automaton?

Parameters

newValue If this is true, Markovian edges are not explored from probabilistic states

Returns: this

Definition at line 256 of file BuilderOptions.cpp.

◆ setBuildAllLabels()

BuilderOptions & storm::builder::BuilderOptions::setBuildAllLabels ( bool newValue = true )

Should all reward models be built? If not set, only required reward models are build.

Parameters

newValue The new value (default true)

Returns: this

Definition at line 228 of file BuilderOptions.cpp.

◆ setBuildAllRewardModels()

BuilderOptions & storm::builder::BuilderOptions::setBuildAllRewardModels ( bool newValue = true )

Should all reward models be built? If not set, only required reward models are build.

Parameters

newValue The new value (default true)

Returns: this

Definition at line 196 of file BuilderOptions.cpp.

◆ setBuildChoiceLabels()

BuilderOptions & storm::builder::BuilderOptions::setBuildChoiceLabels ( bool newValue = true )

Should the choice labels be built?

Parameters

newValue The new value (default true)

Returns: this

Definition at line 261 of file BuilderOptions.cpp.

◆ setBuildChoiceOrigins()

BuilderOptions & storm::builder::BuilderOptions::setBuildChoiceOrigins ( bool newValue = true )

Should the origins the different choices be built?

Parameters

newValue The new value (default true)

Returns: this

Definition at line 276 of file BuilderOptions.cpp.

◆ setBuildObservationValuations()

BuilderOptions & storm::builder::BuilderOptions::setBuildObservationValuations ( bool newValue = true )

Should a observation valuation mapping be built?

Parameters

newValue The new value (default true)

Returns: this

Definition at line 271 of file BuilderOptions.cpp.

◆ setBuildStateValuations()

BuilderOptions & storm::builder::BuilderOptions::setBuildStateValuations ( bool newValue = true )

Should the state valuation mapping be built?

Parameters

newValue The new value (default true)

Returns: this

Definition at line 266 of file BuilderOptions.cpp.

◆ setExplorationChecks()

BuilderOptions & storm::builder::BuilderOptions::setExplorationChecks ( bool newValue = true )

Should extra checks be performed during exploration.

Parameters

newValue The new value (default true)

Returns: this

Definition at line 217 of file BuilderOptions.cpp.

◆ setInferObservationsFromActions()

BuilderOptions & storm::builder::BuilderOptions::setInferObservationsFromActions ( bool newValue = true )

◆ setReservedBitsForUnboundedVariables()

BuilderOptions & storm::builder::BuilderOptions::setReservedBitsForUnboundedVariables ( uint64_t value )

Sets the number of bits that will be reserved for unbounded integer variables.

Definition at line 291 of file BuilderOptions.cpp.

◆ setScaleAndLiftTransitionRewards()

BuilderOptions & storm::builder::BuilderOptions::setScaleAndLiftTransitionRewards ( bool newValue = true )

Should extra checks be performed during exploration.

Parameters

newValue The new value (default true)

Returns: this

Definition at line 281 of file BuilderOptions.cpp.

◆ setTerminalStatesFromFormula()

void storm::builder::BuilderOptions::setTerminalStatesFromFormula ( storm::logic::Formula const & formula )

Analyzes the given formula and sets an expression for the states states of the model that can be treated as terminal states.

Note that this may interfere with checking properties different than the one provided.

Parameters

formula The formula used to (possibly) derive an expression for the terminal states of the model.

Definition at line 118 of file BuilderOptions.cpp.

◆ substituteExpressions()

BuilderOptions & storm::builder::BuilderOptions::substituteExpressions ( std::function< storm::expressions::Expression(storm::expressions::Expression const &)> const & substitutionFunction )

Substitutes all expressions occurring in these options.

Definition at line 301 of file BuilderOptions.cpp.

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

src/storm/builder/BuilderOptions.h
src/storm/builder/BuilderOptions.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ BuilderOptions() [1/3]

◆ BuilderOptions() [2/3]

◆ BuilderOptions() [3/3]

Member Function Documentation

◆ addLabel() [1/2]

◆ addLabel() [2/2]

◆ addRewardModel()

◆ addTerminalExpression()

◆ addTerminalLabel()

◆ clearTerminalStates()

◆ getExpressionLabels()

◆ getLabelNames()

◆ getReservedBitsForUnboundedVariables()

◆ getRewardModelNames()

◆ getShowProgressDelay()

◆ getStochasticTolerance()

◆ getTerminalStates()

◆ hasTerminalStates()

◆ isAddOutOfBoundsStateSet()

◆ isAddOverlappingGuardLabelSet()

◆ isApplyMaximalProgressAssumptionSet()

◆ isBuildAllLabelsSet()

◆ isBuildAllRewardModelsSet()

◆ isBuildChoiceLabelsSet()

◆ isBuildChoiceOriginsSet()

◆ isBuildObservationValuationsSet()

◆ isBuildStateValuationsSet()

◆ isExplorationChecksSet()

◆ isInferObservationsFromActionsSet()

◆ isScaleAndLiftTransitionRewardsSet()

◆ isShowProgressSet()

◆ preserveFormula()

◆ setAddOutOfBoundsState()

◆ setAddOverlappingGuardsLabel()

◆ setApplyMaximalProgressAssumption()

◆ setBuildAllLabels()

◆ setBuildAllRewardModels()

◆ setBuildChoiceLabels()

◆ setBuildChoiceOrigins()

◆ setBuildObservationValuations()

◆ setBuildStateValuations()

◆ setExplorationChecks()

◆ setInferObservationsFromActions()

◆ setReservedBitsForUnboundedVariables()

◆ setScaleAndLiftTransitionRewards()

◆ setTerminalStatesFromFormula()

◆ substituteExpressions()