Storm
A Modern Probabilistic Model Checker
|
This class represents the settings for the abstraction procedures. More...
#include <AbstractionSettings.h>
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. | |
![]() | |
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::SettingMemento > | overrideOption (std::string const &name, bool requiredStatus) |
Sets the option with the given name to the required status. | |
std::string const & | getModuleName () const |
Retrieves the name of the module to which these settings belong. | |
std::vector< std::shared_ptr< Option > > const & | getOptions () 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 | |
![]() | |
Option & | getOption (std::string const &longName) |
Retrieves the option with the given long name. | |
Option const & | getOption (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. | |
This class represents the settings for the abstraction procedures.
Definition at line 12 of file AbstractionSettings.h.
Enumerator | |
---|---|
Games | |
Bisimulation |
Definition at line 14 of file AbstractionSettings.h.
Enumerator | |
---|---|
NearestMaximalDeviation | |
MostProbablePath | |
MaxWeightedDeviation |
Definition at line 16 of file AbstractionSettings.h.
Enumerator | |
---|---|
All | |
None | |
Qualitative | |
Quantitative |
Definition at line 20 of file AbstractionSettings.h.
Enumerator | |
---|---|
Dd | |
Sparse |
Definition at line 22 of file AbstractionSettings.h.
Enumerator | |
---|---|
All | |
None | |
NonGuard |
Definition at line 18 of file AbstractionSettings.h.
Enumerator | |
---|---|
MorePredicates | |
BlockEnumeration |
Definition at line 24 of file AbstractionSettings.h.
storm::settings::modules::AbstractionSettings::AbstractionSettings | ( | ) |
Creates a new set of abstraction settings.
Definition at line 38 of file AbstractionSettings.cpp.
AbstractionSettings::Method storm::settings::modules::AbstractionSettings::getAbstractionRefinementMethod | ( | ) | const |
Retrieves the selected abstraction refinement method.
Definition at line 219 of file AbstractionSettings.cpp.
std::string storm::settings::modules::AbstractionSettings::getConstraintString | ( | ) | const |
Retrieves the string that specifies additional constraints.
Definition at line 323 of file AbstractionSettings.cpp.
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.
uint_fast64_t storm::settings::modules::AbstractionSettings::getMaximalAbstractionCount | ( | ) | const |
Retrieves the maximal number of abstractions to perform until giving up on converging.
Definition at line 311 of file AbstractionSettings.cpp.
AbstractionSettings::PivotSelectionHeuristic storm::settings::modules::AbstractionSettings::getPivotSelectionHeuristic | ( | ) | const |
Retrieves the selected heuristic to select pivot blocks.
Definition at line 285 of file AbstractionSettings.cpp.
double storm::settings::modules::AbstractionSettings::getPrecision | ( | ) | const |
Retrieves the precision that is used for detecting convergence.
Definition at line 277 of file AbstractionSettings.cpp.
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.
AbstractionSettings::ReuseMode storm::settings::modules::AbstractionSettings::getReuseMode | ( | ) | const |
Retrieves the selected reuse mode.
Definition at line 297 of file AbstractionSettings.cpp.
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.
AbstractionSettings::SplitMode storm::settings::modules::AbstractionSettings::getSplitMode | ( | ) | const |
Retrieves the selected split mode.
Definition at line 233 of file AbstractionSettings.cpp.
AbstractionSettings::ValidBlockMode storm::settings::modules::AbstractionSettings::getValidBlockMode | ( | ) | const |
Retrieves the selected mode to guarantee valid blocks.
Definition at line 351 of file AbstractionSettings.cpp.
bool storm::settings::modules::AbstractionSettings::isAddAllGuardsSet | ( | ) | const |
Retrieves whether the option to add all guards was set.
Definition at line 253 of file AbstractionSettings.cpp.
bool storm::settings::modules::AbstractionSettings::isAddAllInitialExpressionsSet | ( | ) | const |
Retrieves whether the option to add all initial expressions was set.
Definition at line 257 of file AbstractionSettings.cpp.
bool storm::settings::modules::AbstractionSettings::isConstraintsSet | ( | ) | const |
Retrieves whether the constraints option was set.
Definition at line 319 of file AbstractionSettings.cpp.
bool storm::settings::modules::AbstractionSettings::isDebugSet | ( | ) | const |
Retrieves whether the debug option was set.
Definition at line 331 of file AbstractionSettings.cpp.
bool storm::settings::modules::AbstractionSettings::isFixPlayer1StrategySet | ( | ) | const |
Retrieves whether player 1 strategies are to be fixed.
Definition at line 343 of file AbstractionSettings.cpp.
bool storm::settings::modules::AbstractionSettings::isFixPlayer2StrategySet | ( | ) | const |
Retrieves whether player 2 strategies are to be fixed.
Definition at line 347 of file AbstractionSettings.cpp.
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.
bool storm::settings::modules::AbstractionSettings::isRankRefinementPredicatesSet | ( | ) | const |
Definition at line 315 of file AbstractionSettings.cpp.
bool storm::settings::modules::AbstractionSettings::isRestrictToRelevantStatesSet | ( | ) | const |
Retrieves whether only relevant states are to be considered.
Definition at line 273 of file AbstractionSettings.cpp.
bool storm::settings::modules::AbstractionSettings::isUseDecompositionSet | ( | ) | const |
Retrieves whether the option to use the decomposition was set.
Definition at line 229 of file AbstractionSettings.cpp.
bool storm::settings::modules::AbstractionSettings::isUseEagerRefinementSet | ( | ) | const |
Retrieves whether to refine eagerly.
Definition at line 327 of file AbstractionSettings.cpp.
bool storm::settings::modules::AbstractionSettings::isUseInterpolationSet | ( | ) | const |
Retrieves whether the option to use interpolation was set.
Definition at line 269 of file AbstractionSettings.cpp.
Sets the option to add all guards to the specified value.
value | The new value. |
Definition at line 261 of file AbstractionSettings.cpp.
Sets the option to add all initial expressions to the specified value.
value | The new value. |
Definition at line 265 of file AbstractionSettings.cpp.
|
static |
Definition at line 186 of file AbstractionSettings.h.