Storm
A Modern Probabilistic Model Checker
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Public Member Functions | List of all members
storm::builder::BuilderOptions Class Reference

#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
 
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 41 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
formulaThe formula based on which to choose the building options.

Definition at line 60 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
formulaThes formula based on which to choose the building options.

Definition at line 65 of file BuilderOptions.cpp.

Member Function Documentation

◆ addLabel() [1/2]

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

Definition at line 233 of file BuilderOptions.cpp.

◆ addLabel() [2/2]

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

Definition at line 226 of file BuilderOptions.cpp.

◆ addRewardModel()

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

Add an additional reward model to build.

Parameters
newValueThe name of the extra reward model
Returns
this

Definition at line 215 of file BuilderOptions.cpp.

◆ addTerminalExpression()

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

Definition at line 239 of file BuilderOptions.cpp.

◆ addTerminalLabel()

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

Definition at line 244 of file BuilderOptions.cpp.

◆ clearTerminalStates()

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

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

◆ getLabelNames()

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

Which labels are built.

Returns

Definition at line 125 of file BuilderOptions.cpp.

◆ getReservedBitsForUnboundedVariables()

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

Definition at line 185 of file BuilderOptions.cpp.

◆ getRewardModelNames()

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

Which reward models are built.

Returns

Definition at line 121 of file BuilderOptions.cpp.

◆ getShowProgressDelay()

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

Definition at line 206 of file BuilderOptions.cpp.

◆ getTerminalStates()

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

Definition at line 133 of file BuilderOptions.cpp.

◆ hasTerminalStates()

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

Definition at line 137 of file BuilderOptions.cpp.

◆ isAddOutOfBoundsStateSet()

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

Definition at line 181 of file BuilderOptions.cpp.

◆ isAddOverlappingGuardLabelSet()

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

Definition at line 189 of file BuilderOptions.cpp.

◆ isApplyMaximalProgressAssumptionSet()

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

Definition at line 145 of file BuilderOptions.cpp.

◆ isBuildAllLabelsSet()

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

Definition at line 169 of file BuilderOptions.cpp.

◆ isBuildAllRewardModelsSet()

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

Definition at line 165 of file BuilderOptions.cpp.

◆ isBuildChoiceLabelsSet()

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

Definition at line 149 of file BuilderOptions.cpp.

◆ isBuildChoiceOriginsSet()

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

Definition at line 161 of file BuilderOptions.cpp.

◆ isBuildObservationValuationsSet()

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

Definition at line 157 of file BuilderOptions.cpp.

◆ isBuildStateValuationsSet()

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

Definition at line 153 of file BuilderOptions.cpp.

◆ isExplorationChecksSet()

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

Definition at line 198 of file BuilderOptions.cpp.

◆ isInferObservationsFromActionsSet()

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

Definition at line 173 of file BuilderOptions.cpp.

◆ isScaleAndLiftTransitionRewardsSet()

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

Definition at line 177 of file BuilderOptions.cpp.

◆ isShowProgressSet()

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

Definition at line 202 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
formulaThe formula that is to be ''preserved''.

Definition at line 87 of file BuilderOptions.cpp.

◆ setAddOutOfBoundsState()

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

Should a state for out of bounds be constructed.

Parameters
newValueThe new value (default true)
Returns
this

Definition at line 279 of file BuilderOptions.cpp.

◆ setAddOverlappingGuardsLabel()

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

Should a state be labelled for overlapping guards.

Parameters
newValuethe new value (default true)

Definition at line 289 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
newValueIf this is true, Markovian edges are not explored from probabilistic states
Returns
this

Definition at line 249 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
newValueThe new value (default true)
Returns
this

Definition at line 221 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
newValueThe new value (default true)
Returns
this

Definition at line 193 of file BuilderOptions.cpp.

◆ setBuildChoiceLabels()

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

Should the choice labels be built?

Parameters
newValueThe new value (default true)
Returns
this

Definition at line 254 of file BuilderOptions.cpp.

◆ setBuildChoiceOrigins()

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

Should the origins the different choices be built?

Parameters
newValueThe new value (default true)
Returns
this

Definition at line 269 of file BuilderOptions.cpp.

◆ setBuildObservationValuations()

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

Should a observation valuation mapping be built?

Parameters
newValueThe new value (default true)
Returns
this

Definition at line 264 of file BuilderOptions.cpp.

◆ setBuildStateValuations()

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

Should the state valuation mapping be built?

Parameters
newValueThe new value (default true)
Returns
this

Definition at line 259 of file BuilderOptions.cpp.

◆ setExplorationChecks()

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

Should extra checks be performed during exploration.

Parameters
newValueThe new value (default true)
Returns
this

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

◆ setScaleAndLiftTransitionRewards()

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

Should extra checks be performed during exploration.

Parameters
newValueThe new value (default true)
Returns
this

Definition at line 274 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
formulaThe formula used to (possibly) derive an expression for the terminal states of the model.

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

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