Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BeliefExplorationSettings.cpp
Go to the documentation of this file.
2
8
9namespace storm {
10namespace settings {
11namespace modules {
12
13const std::string BeliefExplorationSettings::moduleName = "beliefExploration";
14
15const std::string refineOption = "refine";
16const std::string explorationTimeLimitOption = "exploration-time";
17const std::string resolutionOption = "resolution";
18const std::string clipGridResolutionOption = "clip-resolution";
19const std::string sizeThresholdOption = "size-threshold";
20const std::string gapThresholdOption = "gap-threshold";
21const std::string optimalChoiceValueThresholdOption = "optimal-choice-value-threshold";
22const std::string observationThresholdOption = "obs-threshold";
23const std::string numericPrecisionOption = "numeric-precision";
24const std::string triangulationModeOption = "triangulationmode";
25const std::string clippingOption = "use-clipping";
26const std::string cutZeroGapOption = "cut-zero-gap";
27const std::string stateEliminationCutoffOption = "state-elimination-cutoff";
28
30 this->addOption(
32 "Refines the result bounds until reaching either the goal precision or the refinement step limit")
33 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("prec", "The goal precision.")
34 .setDefaultValueDouble(1e-4)
35 .makeOptional()
37 .build())
38 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("steps", "The number of allowed refinement steps (0 means no limit).")
39 .setDefaultValueUnsignedInteger(0)
40 .makeOptional()
41 .build())
42 .build());
43
44 this->addOption(
45 storm::settings::OptionBuilder(moduleName, explorationTimeLimitOption, false, "Sets after which time no further states shall be explored.")
46 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "In seconds.").setDefaultValueUnsignedInteger(0).build())
47 .build());
48
49 this->addOption(
51 "Sets the resolution of the discretization and how it is increased in case of refinement")
52 .setIsAdvanced()
53 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("init", "the initial resolution (higher means more precise)")
54 .setDefaultValueUnsignedInteger(2)
56 .build())
58 "factor", "Multiplied to the resolution of refined observations (higher means more precise).")
59 .setDefaultValueDouble(2)
60 .makeOptional()
62 .build())
63 .build());
64
65 this->addOption(storm::settings::OptionBuilder(moduleName, clipGridResolutionOption, false, "Sets the resolution of the clipping grid")
66 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("resolution", "the resolution (higher means more precise)")
67 .setDefaultValueUnsignedInteger(2)
69 .build())
70 .build());
71
72 this->addOption(
73 storm::settings::OptionBuilder(moduleName, observationThresholdOption, false, "Only observations whose score is below this threshold will be refined.")
74 .setIsAdvanced()
75 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("init", "initial threshold (higher means more precise")
76 .setDefaultValueDouble(0.1)
78 .build())
80 "factor", "Controlls how fast the threshold is increased in each refinement step (higher means more precise).")
81 .setDefaultValueDouble(0.1)
82 .makeOptional()
84 .build())
85 .build());
86
87 this->addOption(
90 "Sets how many new states are explored or rewired in a refinement step and how this value is increased in case of refinement.")
91 .setIsAdvanced()
92 .addArgument(
93 storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("init", "initial limit (higher means more precise, 0 means automatic choice)")
94 .setDefaultValueUnsignedInteger(0)
95 .build())
97 "factor", "Before each step the new threshold is set to the current state count times this number (higher means more precise).")
98 .setDefaultValueDouble(4)
99 .makeOptional()
101 .build())
102 .build());
103
104 this->addOption(
106 "Sets how large the gap between known lower- and upper bounds at a beliefstate needs to be in order to explore")
107 .setIsAdvanced()
108 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("init", "initial threshold (higher means less precise")
109 .setDefaultValueDouble(0.1)
111 .build())
112 .addArgument(
113 storm::settings::ArgumentBuilder::createDoubleArgument("factor", "Multiplied to the gap in each refinement step (higher means less precise).")
114 .setDefaultValueDouble(0.25)
115 .makeOptional()
117 .build())
118 .build());
119
121 "Sets how much worse a sub-optimal choice can be in order to be included in the relevant explored fragment")
122 .setIsAdvanced()
123 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("init", "initial threshold (higher means more precise")
124 .setDefaultValueDouble(1e-3)
126 .build())
128 "factor", "Multiplied to the threshold in each refinement step (higher means more precise).")
129 .setDefaultValueDouble(1)
130 .makeOptional()
132 .build())
133 .build());
134
135 this->addOption(
136 storm::settings::OptionBuilder(moduleName, numericPrecisionOption, false, "Sets the precision used to determine whether two belief-states are equal.")
137 .setIsAdvanced()
138 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "the precision")
139 .setDefaultValueDouble(1e-9)
140 .makeOptional()
142 .build())
143 .build());
144
145 this->addOption(storm::settings::OptionBuilder(moduleName, triangulationModeOption, false, "Sets how to triangulate beliefs when discretizing.")
146 .setIsAdvanced()
147 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "the triangulation mode")
148 .setDefaultValueString("dynamic")
149 .addValidatorString(storm::settings::ArgumentValidatorFactory::createMultipleChoiceValidator({"dynamic", "static"}))
150 .build())
151 .build());
152 this->addOption(
153 storm::settings::OptionBuilder(moduleName, clippingOption, false, "If this is set, unfolding will use (grid) clipping instead of cut-offs only.")
154 .build());
155 this->addOption(
156 storm::settings::OptionBuilder(moduleName, cutZeroGapOption, false, "Cut beliefs where the gap between over- and underapproximation is 0.").build());
158 "If this is set, an additional unfolding step for cut-off beliefs is performed.")
159 .build());
160}
161
163 return this->getOption(refineOption).getHasOptionBeenSet();
164}
165
167 return this->getOption(stateEliminationCutoffOption).getHasOptionBeenSet();
168}
169
171 return this->getOption(refineOption).getArgumentByName("prec").getValueAsDouble();
172}
173
175 return this->getOption(refineOption).getArgumentByName("steps").getValueAsUnsignedInteger();
176}
177
179 return this->getOption(explorationTimeLimitOption).getArgumentByName("time").getValueAsUnsignedInteger();
180}
181
183 return this->getOption(resolutionOption).getArgumentByName("init").getValueAsUnsignedInteger();
184}
185
187 return this->getOption(clipGridResolutionOption).getArgumentByName("resolution").getValueAsUnsignedInteger();
188}
189
191 return this->getOption(resolutionOption).getArgumentByName("factor").getValueAsDouble();
192}
193
195 return this->getOption(sizeThresholdOption).getArgumentByName("init").getValueAsUnsignedInteger();
196}
197
199 return this->getOption(sizeThresholdOption).getArgumentByName("factor").getValueAsDouble();
200}
201
203 return this->getOption(gapThresholdOption).getArgumentByName("init").getValueAsDouble();
204}
205
207 return this->getOption(gapThresholdOption).getArgumentByName("factor").getValueAsDouble();
208}
209
211 return this->getOption(optimalChoiceValueThresholdOption).getArgumentByName("init").getValueAsDouble();
212}
213
215 return this->getOption(optimalChoiceValueThresholdOption).getArgumentByName("factor").getValueAsDouble();
216}
217
219 return this->getOption(observationThresholdOption).getArgumentByName("init").getValueAsDouble();
220}
221
223 return this->getOption(observationThresholdOption).getArgumentByName("factor").getValueAsDouble();
224}
225
227 return !this->getOption(numericPrecisionOption).getHasOptionBeenSet() ||
228 this->getOption(numericPrecisionOption).getArgumentByName("value").wasSetFromDefaultValue();
229}
230
232 return this->getOption(numericPrecisionOption).getArgumentByName("value").getValueAsDouble();
233}
234
236 return this->getOption(triangulationModeOption).getArgumentByName("value").getValueAsString() == "dynamic";
237}
239 return this->getOption(triangulationModeOption).getArgumentByName("value").getValueAsString() == "static";
240}
241
243 return this->getOption(clippingOption).getHasOptionBeenSet();
244}
245
247 return this->getOption(cutZeroGapOption).getHasOptionBeenSet();
248}
249
250template<typename ValueType>
252 options.refine = isRefineSet();
253 options.refinePrecision = storm::utility::convertNumber<ValueType>(getRefinePrecision());
256
259 options.resolutionFactor = storm::utility::convertNumber<ValueType>(getResolutionFactor());
261 options.sizeThresholdFactor = storm::utility::convertNumber<ValueType>(getSizeThresholdFactor());
262 options.gapThresholdInit = storm::utility::convertNumber<ValueType>(getGapThresholdInit());
263 options.gapThresholdFactor = storm::utility::convertNumber<ValueType>(getGapThresholdFactor());
264 options.optimalChoiceValueThresholdInit = storm::utility::convertNumber<ValueType>(getOptimalChoiceValueThresholdInit());
265 options.optimalChoiceValueThresholdFactor = storm::utility::convertNumber<ValueType>(getOptimalChoiceValueThresholdFactor());
266 options.obsThresholdInit = storm::utility::convertNumber<ValueType>(getObservationScoreThresholdInit());
267 options.obsThresholdIncrementFactor = storm::utility::convertNumber<ValueType>(getObservationScoreThresholdFactor());
268 options.useClipping = isUseClippingSet();
270
271 options.numericPrecision = storm::utility::convertNumber<ValueType>(getNumericPrecision());
274 STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "Setting numeric precision to zero because exact arithmethic is used.");
275 options.numericPrecision = storm::utility::zero<ValueType>();
276 } else {
278 "A non-zero numeric precision was set although exact arithmethic is used. Results might be inexact.");
279 }
280 }
282 options.cutZeroGap = isCutZeroGapSet();
283}
284
285template void BeliefExplorationSettings::setValuesInOptionsStruct<double>(
287template void BeliefExplorationSettings::setValuesInOptionsStruct<storm::RationalNumber>(
289
290} // namespace modules
291} // namespace settings
292} // 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.
virtual bool wasSetFromDefaultValue() const =0
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 > > createDoubleGreaterValidator(double lowerBound)
static std::shared_ptr< ArgumentValidator< uint64_t > > createUnsignedGreaterValidator(uint64_t lowerBound)
static std::shared_ptr< ArgumentValidator< double > > createDoubleGreaterEqualValidator(double lowerBound)
static std::shared_ptr< ArgumentValidator< std::string > > createMultipleChoiceValidator(std::vector< std::string > const &choices)
static std::shared_ptr< ArgumentValidator< double > > createDoubleRangeValidatorIncluding(double lowerBound, double upperBound)
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
uint64_t getClippingGridResolution() const
Clipping Grid Resolution.
double getGapThresholdInit() const
Controls how large the gap between known lower- and upper bounds at a beliefstate needs to be in orde...
double getObservationScoreThresholdInit() const
Controls which observations are refined.
BeliefExplorationSettings()
Creates a new set of POMDP settings.
uint64_t getSizeThresholdInit() const
The maximal number of newly expanded MDP states in a refinement step.
bool isUseClippingSet() const
Controls if (grid) clipping is to be used.
double getOptimalChoiceValueThresholdInit() const
Controls whether "almost optimal" choices will be considered optimal.
void setValuesInOptionsStruct(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions< ValueType > &options) const
bool isNumericPrecisionSetFromDefault() const
Used to determine whether two beliefs are equal.
uint64_t getResolutionInit() const
Discretization Resolution.
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
const std::string optimalChoiceValueThresholdOption
bool isZero(ValueType const &a)
Definition constants.cpp:39