Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExplorationSettings.cpp
Go to the documentation of this file.
8
12
13namespace storm {
14namespace settings {
15namespace modules {
16
17const std::string ExplorationSettings::moduleName = "exploration";
18const std::string ExplorationSettings::precomputationTypeOptionName = "precomp";
19const std::string ExplorationSettings::numberOfExplorationStepsUntilPrecomputationOptionName = "stepsprecomp";
20const std::string ExplorationSettings::numberOfSampledPathsUntilPrecomputationOptionName = "pathsprecomp";
21const std::string ExplorationSettings::nextStateHeuristicOptionName = "nextstate";
22const std::string ExplorationSettings::precisionOptionName = "precision";
23const std::string ExplorationSettings::precisionOptionShortName = "eps";
24
26 std::vector<std::string> types = {"local", "global"};
27 this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used.")
28 .setIsAdvanced()
29 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.")
31 .setDefaultValueString("global")
32 .build())
33 .build());
34 this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, true,
35 "Sets the number of exploration steps to perform until a precomputation is triggered.")
36 .setIsAdvanced()
37 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.")
39 .build())
40 .build());
41 this->addOption(storm::settings::OptionBuilder(moduleName, numberOfSampledPathsUntilPrecomputationOptionName, true,
42 "If set, a precomputation is perfomed periodically after the given number of paths has been sampled.")
43 .setIsAdvanced()
45 "count", "The number of paths to sample until a precomputation is triggered.")
47 .build())
48 .build());
49
50 std::vector<std::string> nextStateHeuristics = {"probdiffs", "prob", "unif"};
51 this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use.")
52 .setIsAdvanced()
54 "name",
55 "The name of the heuristic to use. 'prob' samples according to the probabilities in the system, 'probdiffs' takes "
56 "into account probabilities and the differences between the current bounds and 'unif' samples uniformly.")
58 .setDefaultValueString("probdiffs")
59 .build())
60 .build());
61
62 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision to achieve.")
63 .setShortName(precisionOptionShortName)
64 .setIsAdvanced()
65 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The value to use to determine convergence.")
68 .build())
69 .build());
70}
71
73 if (this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString() == "local") {
74 return true;
75 }
76 return false;
77}
78
80 if (this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString() == "global") {
81 return true;
82 }
83 return false;
84}
85
87 std::string typeAsString = this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString();
88 if (typeAsString == "local") {
90 } else if (typeAsString == "global") {
92 }
93 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown precomputation type '" << typeAsString << "'.");
94}
95
97 return this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
98}
99
101 return this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet();
102}
103
105 return this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
106}
107
109 std::string nextStateHeuristicAsString = this->getOption(nextStateHeuristicOptionName).getArgumentByName("name").getValueAsString();
110 if (nextStateHeuristicAsString == "probdiffs") {
112 } else if (nextStateHeuristicAsString == "prob") {
114 } else if (nextStateHeuristicAsString == "unif") {
116 }
117 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown next-state heuristic '" << nextStateHeuristicAsString << "'.");
118}
119
121 return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
122}
123
125 bool optionsSet = this->getOption(precomputationTypeOptionName).getHasOptionBeenSet() ||
126 this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() ||
127 this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet() ||
128 this->getOption(nextStateHeuristicOptionName).getHasOptionBeenSet();
130 "Exploration engine is not selected, so setting options for it has no effect.");
131 return true;
132}
133} // namespace modules
134} // namespace settings
135} // namespace storm
virtual std::string getValueAsString() const =0
Retrieves the value of this argument as a string.
virtual uint_fast64_t getValueAsUnsignedInteger() const =0
Retrieves the value of this argument as an unsigned integer.
virtual double getValueAsDouble() const =0
Retrieves the value of this argument as a double.
static ArgumentBuilder createUnsignedIntegerArgument(std::string const &name, std::string const &description)
Creates an unsigned integer argument with the given parameters.
static ArgumentBuilder createDoubleArgument(std::string const &name, std::string const &description)
Creates a double argument with the given parameters.
static ArgumentBuilder createStringArgument(std::string const &name, std::string const &description)
Creates a string argument with the given parameters.
static std::shared_ptr< ArgumentValidator< double > > createDoubleRangeValidatorExcluding(double lowerBound, double upperBound)
static std::shared_ptr< ArgumentValidator< std::string > > createMultipleChoiceValidator(std::vector< std::string > const &choices)
This class provides the interface to create an option...
ArgumentBase const & getArgumentByName(std::string const &argumentName) const
Returns a reference to the argument with the specified long name.
Definition Option.cpp:79
bool getHasOptionBeenSet() const
Retrieves whether the option has been set.
Definition Option.cpp:125
uint_fast64_t getNumberOfSampledPathsUntilPrecomputation() const
Retrieves the number of paths to sample until a precomputation is triggered.
bool isLocalPrecomputationSet() const
Retrieves whether local precomputation is to be used.
uint_fast64_t getNumberOfExplorationStepsUntilPrecomputation() const
Retrieves the number of exploration steps to perform until a precomputation is triggered.
double getPrecision() const
Retrieves the precision to use for numerical operations.
NextStateHeuristic getNextStateHeuristic() const
Retrieves the selected next-state heuristic.
PrecomputationType getPrecomputationType() const
Retrieves the selected precomputation type.
ExplorationSettings()
Creates a new set of exploration settings.
bool isGlobalPrecomputationSet() const
Retrieves whether global precomputation is to be used.
virtual bool check() const override
Checks whether the settings are consistent.
This is the base class of the settings for a particular module.
void addOption(std::shared_ptr< Option > const &option)
Adds and registers the given option.
Option & getOption(std::string const &longName)
Retrieves the option with the given long name.
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SettingsType const & getModule()
Get module.
LabParser.cpp.
Definition cli.cpp:18