Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm::settings::modules::AbstractionSettings Class Reference

This class represents the settings for the abstraction procedures. More...

#include <AbstractionSettings.h>

Inheritance diagram for storm::settings::modules::AbstractionSettings:
Collaboration diagram for storm::settings::modules::AbstractionSettings:

Public Types

enum class  Method { Games , Bisimulation }
 
enum class  PivotSelectionHeuristic { NearestMaximalDeviation , MostProbablePath , MaxWeightedDeviation }
 
enum class  SplitMode { All , None , NonGuard }
 
enum class  ReuseMode { All , None , Qualitative , Quantitative }
 
enum class  SolveMode { Dd , Sparse }
 
enum class  ValidBlockMode { MorePredicates , BlockEnumeration }
 

Public Member Functions

 AbstractionSettings ()
 Creates a new set of abstraction settings.
 
Method getAbstractionRefinementMethod () const
 Retrieves the selected abstraction refinement method.
 
bool isUseDecompositionSet () const
 Retrieves whether the option to use the decomposition was set.
 
SplitMode getSplitMode () const
 Retrieves the selected split mode.
 
bool isAddAllGuardsSet () const
 Retrieves whether the option to add all guards was set.
 
bool isAddAllInitialExpressionsSet () const
 Retrieves whether the option to add all initial expressions was set.
 
void setAddAllGuards (bool value)
 Sets the option to add all guards to the specified value.
 
void setAddAllInitialExpressions (bool value)
 Sets the option to add all initial expressions to the specified value.
 
bool isUseInterpolationSet () const
 Retrieves whether the option to use interpolation was set.
 
double getPrecision () const
 Retrieves the precision that is used for detecting convergence.
 
bool getRelativeTerminationCriterion () const
 Retrieves whether to use a relative termination criterion for detecting convergence.
 
PivotSelectionHeuristic getPivotSelectionHeuristic () const
 Retrieves the selected heuristic to select pivot blocks.
 
ReuseMode getReuseMode () const
 Retrieves the selected reuse mode.
 
bool isRestrictToRelevantStatesSet () const
 Retrieves whether only relevant states are to be considered.
 
SolveMode getSolveMode () const
 Retrieves the mode with which to solve the games.
 
uint_fast64_t getMaximalAbstractionCount () const
 Retrieves the maximal number of abstractions to perform until giving up on converging.
 
bool isRankRefinementPredicatesSet () const
 
bool isConstraintsSet () const
 Retrieves whether the constraints option was set.
 
std::string getConstraintString () const
 Retrieves the string that specifies additional constraints.
 
bool isUseEagerRefinementSet () const
 Retrieves whether to refine eagerly.
 
bool isDebugSet () const
 Retrieves whether the debug option was set.
 
bool isInjectRefinementPredicatesSet () const
 Retrieves whether the option to inject the refinement predicates is set.
 
std::string getInjectedRefinementPredicates () const
 Retrieves a string containing refinement predicates to inject (if there are any).
 
bool isFixPlayer1StrategySet () const
 Retrieves whether player 1 strategies are to be fixed.
 
bool isFixPlayer2StrategySet () const
 Retrieves whether player 2 strategies are to be fixed.
 
ValidBlockMode getValidBlockMode () const
 Retrieves the selected mode to guarantee valid blocks.
 
- Public Member Functions inherited from storm::settings::modules::ModuleSettings
 ModuleSettings (std::string const &moduleName)
 Constructs a new settings object.
 
virtual ~ModuleSettings ()
 
virtual bool check () const
 Checks whether the settings are consistent.
 
virtual void finalize ()
 Prepares the modules for further usage, should be called at the end of the initialization, before checks are executed.
 
std::unique_ptr< storm::settings::SettingMementooverrideOption (std::string const &name, bool requiredStatus)
 Sets the option with the given name to the required status.
 
std::string constgetModuleName () const
 Retrieves the name of the module to which these settings belong.
 
std::vector< std::shared_ptr< Option > > constgetOptions () const
 Retrieves the options of this module.
 
uint_fast64_t getPrintLengthOfLongestOption (bool includeAdvanced) const
 Retrieves the (print) length of the longest option.
 
void restoreDefaults ()
 Restores the default values for all arguments of all options.
 

Static Public Attributes

static const std::string moduleName = "abstraction"
 

Additional Inherited Members

- Protected Member Functions inherited from storm::settings::modules::ModuleSettings
OptiongetOption (std::string const &longName)
 Retrieves the option with the given long name.
 
Option constgetOption (std::string const &longName) const
 Retrieves the option with the given long name.
 
bool isSet (std::string const &optionName) const
 Retrieves whether the option with the given name was set.
 
void set (std::string const &name)
 Sets the option with the specified name.
 
void unset (std::string const &name)
 Unsets the option with the specified name.
 
void addOption (std::shared_ptr< Option > const &option)
 Adds and registers the given option.
 

Detailed Description

This class represents the settings for the abstraction procedures.

Definition at line 12 of file AbstractionSettings.h.

Member Enumeration Documentation

◆ Method

Enumerator
Games 
Bisimulation 

Definition at line 14 of file AbstractionSettings.h.

◆ PivotSelectionHeuristic

Enumerator
NearestMaximalDeviation 
MostProbablePath 
MaxWeightedDeviation 

Definition at line 16 of file AbstractionSettings.h.

◆ ReuseMode

Enumerator
All 
None 
Qualitative 
Quantitative 

Definition at line 20 of file AbstractionSettings.h.

◆ SolveMode

Enumerator
Dd 
Sparse 

Definition at line 22 of file AbstractionSettings.h.

◆ SplitMode

Enumerator
All 
None 
NonGuard 

Definition at line 18 of file AbstractionSettings.h.

◆ ValidBlockMode

Enumerator
MorePredicates 
BlockEnumeration 

Definition at line 24 of file AbstractionSettings.h.

Constructor & Destructor Documentation

◆ AbstractionSettings()

storm::settings::modules::AbstractionSettings::AbstractionSettings ( )

Creates a new set of abstraction settings.

Definition at line 38 of file AbstractionSettings.cpp.

Member Function Documentation

◆ getAbstractionRefinementMethod()

AbstractionSettings::Method storm::settings::modules::AbstractionSettings::getAbstractionRefinementMethod ( ) const

Retrieves the selected abstraction refinement method.

Definition at line 219 of file AbstractionSettings.cpp.

◆ getConstraintString()

std::string storm::settings::modules::AbstractionSettings::getConstraintString ( ) const

Retrieves the string that specifies additional constraints.

Returns
The string that defines the constraints.

Definition at line 323 of file AbstractionSettings.cpp.

◆ getInjectedRefinementPredicates()

std::string storm::settings::modules::AbstractionSettings::getInjectedRefinementPredicates ( ) const

Retrieves a string containing refinement predicates to inject (if there are any).

Definition at line 339 of file AbstractionSettings.cpp.

◆ getMaximalAbstractionCount()

uint_fast64_t storm::settings::modules::AbstractionSettings::getMaximalAbstractionCount ( ) const

Retrieves the maximal number of abstractions to perform until giving up on converging.

Returns
The maximal abstraction count.

Definition at line 311 of file AbstractionSettings.cpp.

◆ getPivotSelectionHeuristic()

AbstractionSettings::PivotSelectionHeuristic storm::settings::modules::AbstractionSettings::getPivotSelectionHeuristic ( ) const

Retrieves the selected heuristic to select pivot blocks.

Returns
The selected heuristic.

Definition at line 285 of file AbstractionSettings.cpp.

◆ getPrecision()

double storm::settings::modules::AbstractionSettings::getPrecision ( ) const

Retrieves the precision that is used for detecting convergence.

Returns
The precision to use for detecting convergence.

Definition at line 277 of file AbstractionSettings.cpp.

◆ getRelativeTerminationCriterion()

bool storm::settings::modules::AbstractionSettings::getRelativeTerminationCriterion ( ) const

Retrieves whether to use a relative termination criterion for detecting convergence.

Definition at line 281 of file AbstractionSettings.cpp.

◆ getReuseMode()

AbstractionSettings::ReuseMode storm::settings::modules::AbstractionSettings::getReuseMode ( ) const

Retrieves the selected reuse mode.

Returns
The selected reuse mode.

Definition at line 297 of file AbstractionSettings.cpp.

◆ getSolveMode()

AbstractionSettings::SolveMode storm::settings::modules::AbstractionSettings::getSolveMode ( ) const

Retrieves the mode with which to solve the games.

Definition at line 245 of file AbstractionSettings.cpp.

◆ getSplitMode()

AbstractionSettings::SplitMode storm::settings::modules::AbstractionSettings::getSplitMode ( ) const

Retrieves the selected split mode.

Returns
The selected split mode.

Definition at line 233 of file AbstractionSettings.cpp.

◆ getValidBlockMode()

AbstractionSettings::ValidBlockMode storm::settings::modules::AbstractionSettings::getValidBlockMode ( ) const

Retrieves the selected mode to guarantee valid blocks.

Definition at line 351 of file AbstractionSettings.cpp.

◆ isAddAllGuardsSet()

bool storm::settings::modules::AbstractionSettings::isAddAllGuardsSet ( ) const

Retrieves whether the option to add all guards was set.

Returns
True iff the option was set.

Definition at line 253 of file AbstractionSettings.cpp.

◆ isAddAllInitialExpressionsSet()

bool storm::settings::modules::AbstractionSettings::isAddAllInitialExpressionsSet ( ) const

Retrieves whether the option to add all initial expressions was set.

Returns
True iff the option was set.

Definition at line 257 of file AbstractionSettings.cpp.

◆ isConstraintsSet()

bool storm::settings::modules::AbstractionSettings::isConstraintsSet ( ) const

Retrieves whether the constraints option was set.

Returns
True if the constraints option was set.

Definition at line 319 of file AbstractionSettings.cpp.

◆ isDebugSet()

bool storm::settings::modules::AbstractionSettings::isDebugSet ( ) const

Retrieves whether the debug option was set.

Definition at line 331 of file AbstractionSettings.cpp.

◆ isFixPlayer1StrategySet()

bool storm::settings::modules::AbstractionSettings::isFixPlayer1StrategySet ( ) const

Retrieves whether player 1 strategies are to be fixed.

Definition at line 343 of file AbstractionSettings.cpp.

◆ isFixPlayer2StrategySet()

bool storm::settings::modules::AbstractionSettings::isFixPlayer2StrategySet ( ) const

Retrieves whether player 2 strategies are to be fixed.

Definition at line 347 of file AbstractionSettings.cpp.

◆ isInjectRefinementPredicatesSet()

bool storm::settings::modules::AbstractionSettings::isInjectRefinementPredicatesSet ( ) const

Retrieves whether the option to inject the refinement predicates is set.

Definition at line 335 of file AbstractionSettings.cpp.

◆ isRankRefinementPredicatesSet()

bool storm::settings::modules::AbstractionSettings::isRankRefinementPredicatesSet ( ) const

Definition at line 315 of file AbstractionSettings.cpp.

◆ isRestrictToRelevantStatesSet()

bool storm::settings::modules::AbstractionSettings::isRestrictToRelevantStatesSet ( ) const

Retrieves whether only relevant states are to be considered.

Returns
True iff the option was set.

Definition at line 273 of file AbstractionSettings.cpp.

◆ isUseDecompositionSet()

bool storm::settings::modules::AbstractionSettings::isUseDecompositionSet ( ) const

Retrieves whether the option to use the decomposition was set.

Returns
True iff the option was set.

Definition at line 229 of file AbstractionSettings.cpp.

◆ isUseEagerRefinementSet()

bool storm::settings::modules::AbstractionSettings::isUseEagerRefinementSet ( ) const

Retrieves whether to refine eagerly.

Definition at line 327 of file AbstractionSettings.cpp.

◆ isUseInterpolationSet()

bool storm::settings::modules::AbstractionSettings::isUseInterpolationSet ( ) const

Retrieves whether the option to use interpolation was set.

Returns
True iff the option was set.

Definition at line 269 of file AbstractionSettings.cpp.

◆ setAddAllGuards()

void storm::settings::modules::AbstractionSettings::setAddAllGuards ( bool  value)

Sets the option to add all guards to the specified value.

Parameters
valueThe new value.

Definition at line 261 of file AbstractionSettings.cpp.

◆ setAddAllInitialExpressions()

void storm::settings::modules::AbstractionSettings::setAddAllInitialExpressions ( bool  value)

Sets the option to add all initial expressions to the specified value.

Parameters
valueThe new value.

Definition at line 265 of file AbstractionSettings.cpp.

Member Data Documentation

◆ moduleName

const std::string storm::settings::modules::AbstractionSettings::moduleName = "abstraction"
static

Definition at line 186 of file AbstractionSettings.h.


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