#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
double	getStochasticTolerance () const
	Some distributions may not sum to one.
BuilderOptions &	setBuildAllRewardModels (bool newValue=true)
	Should all reward models be built?
BuilderOptions &	addRewardModel (std::string const &rewardModelName)
	Add an additional reward model to build.
BuilderOptions &	setBuildAllLabels (bool newValue=true)
	Should all reward models be built?
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 &	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 &	setStochasticTolerance (double newValue)
	Sets the tolerance used for checking whether a distribution sums to one.
BuilderOptions &	setShowProgress (bool newValue=true)
	Sets whether the progress of state space exploration should be printed.
BuilderOptions &	setShowProgressDelay (uint64_t newValue)
	Sets the delay (in seconds) between progress reports during state space exploration.
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 38 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 58 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 63 of file BuilderOptions.cpp.

Member Function Documentation

◆ addLabel() [1/2]

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

Definition at line 232 of file BuilderOptions.cpp.

◆ addLabel() [2/2]

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

Definition at line 225 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 214 of file BuilderOptions.cpp.

◆ addTerminalExpression()

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

Definition at line 238 of file BuilderOptions.cpp.

◆ addTerminalLabel()

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

Definition at line 243 of file BuilderOptions.cpp.

◆ clearTerminalStates()

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

Definition at line 136 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 124 of file BuilderOptions.cpp.

◆ getLabelNames()

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

Which labels are built.

Returns

Definition at line 120 of file BuilderOptions.cpp.

◆ getReservedBitsForUnboundedVariables()

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

Definition at line 180 of file BuilderOptions.cpp.

◆ getRewardModelNames()

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

Which reward models are built.

Returns

Definition at line 116 of file BuilderOptions.cpp.

◆ getShowProgressDelay()

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

Definition at line 201 of file BuilderOptions.cpp.

◆ getStochasticTolerance()

double storm::builder::BuilderOptions::getStochasticTolerance ( ) const

Some distributions may not sum to one.

This tolerance allows handling this case.

Returns: The tolerance

Definition at line 205 of file BuilderOptions.cpp.

◆ getTerminalStates()

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

Definition at line 128 of file BuilderOptions.cpp.

◆ hasTerminalStates()

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

Definition at line 132 of file BuilderOptions.cpp.

◆ isAddOutOfBoundsStateSet()

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

Definition at line 176 of file BuilderOptions.cpp.

◆ isAddOverlappingGuardLabelSet()

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

Definition at line 184 of file BuilderOptions.cpp.

◆ isApplyMaximalProgressAssumptionSet()

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

Definition at line 140 of file BuilderOptions.cpp.

◆ isBuildAllLabelsSet()

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

Definition at line 164 of file BuilderOptions.cpp.

◆ isBuildAllRewardModelsSet()

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

Definition at line 160 of file BuilderOptions.cpp.

◆ isBuildChoiceLabelsSet()

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

Definition at line 144 of file BuilderOptions.cpp.

◆ isBuildChoiceOriginsSet()

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

Definition at line 156 of file BuilderOptions.cpp.

◆ isBuildObservationValuationsSet()

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

Definition at line 152 of file BuilderOptions.cpp.

◆ isBuildStateValuationsSet()

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

Definition at line 148 of file BuilderOptions.cpp.

◆ isExplorationChecksSet()

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

Definition at line 193 of file BuilderOptions.cpp.

◆ isInferObservationsFromActionsSet()

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

Definition at line 168 of file BuilderOptions.cpp.

◆ isScaleAndLiftTransitionRewardsSet()

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

Definition at line 172 of file BuilderOptions.cpp.

◆ isShowProgressSet()

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

Definition at line 197 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 82 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 278 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 288 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 248 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 220 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 188 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 253 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 268 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 263 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 258 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 209 of file BuilderOptions.cpp.

◆ 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 283 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 273 of file BuilderOptions.cpp.

◆ setShowProgress()

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

Sets whether the progress of state space exploration should be printed.

Parameters

newValue The new value (default true)

Returns: this

Definition at line 298 of file BuilderOptions.cpp.

◆ setShowProgressDelay()

BuilderOptions & storm::builder::BuilderOptions::setShowProgressDelay ( uint64_t newValue )

Sets the delay (in seconds) between progress reports during state space exploration.

Parameters

newValue The new delay

Returns: this

Definition at line 303 of file BuilderOptions.cpp.

◆ setStochasticTolerance()

BuilderOptions & storm::builder::BuilderOptions::setStochasticTolerance ( double newValue )

Sets the tolerance used for checking whether a distribution sums to one.

Parameters

newValue The new tolerance

Returns: this

Definition at line 293 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 110 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 308 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()

◆ setReservedBitsForUnboundedVariables()

◆ setScaleAndLiftTransitionRewards()

◆ setShowProgress()

◆ setShowProgressDelay()

◆ setStochasticTolerance()

◆ setTerminalStatesFromFormula()

◆ substituteExpressions()