Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
IOSettings.h
Go to the documentation of this file.
1#ifndef STORM_SETTINGS_MODULES_IOSETTINGS_H_
2#define STORM_SETTINGS_MODULES_IOSETTINGS_H_
3
4#include <boost/optional.hpp>
5
6#include "storm-config.h"
13
14namespace storm {
15namespace settings {
16namespace modules {
17
21class IOSettings : public ModuleSettings {
22 public:
26 IOSettings();
27
33 bool isExportDotSet() const;
34
40 std::string getExportDotFilename() const;
41
47 size_t getExportDotMaxWidth() const;
48
52 bool isExportBuildSet() const;
53
57 std::string getExportBuildFilename() const;
58
63
68 bool isCompressionSet() const;
69
75
79 bool isExportDigitsSet() const;
80
84 size_t getExportDigits() const;
85
91 bool isExportJaniDotSet() const;
92
98 std::string getExportJaniDotFilename() const;
99
105 bool isExportExplicitSet() const;
106
112 std::string getExportExplicitFilename() const;
113
119 bool isExportDdSet() const;
120
126 std::string getExportDdFilename() const;
127
131 bool isExportCdfSet() const;
132
136 std::string getExportCdfDirectory() const;
137
141 bool isExportSchedulerSet() const;
142
146 std::string getExportSchedulerFilename() const;
147
151 bool isExportCheckResultSet() const;
152
156 std::string getExportCheckResultFilename() const;
157
163 bool isExplicitSet() const;
164
171 std::string getTransitionFilename() const;
172
179 std::string getLabelingFilename() const;
180
186 bool isExplicitDRNSet() const;
187
193 std::string getExplicitDRNFilename() const;
194
200
206 bool isExplicitUmbSet() const;
207
213 std::string getExplicitUmbFilename() const;
214
220 bool isExplicitIMCASet() const;
221
227 std::string getExplicitIMCAFilename() const;
228
234 bool isPrismInputSet() const;
235
241 bool isJaniInputSet() const;
242
248 bool isPrismOrJaniInputSet() const;
249
255 bool isPrismToJaniSet() const;
256
263 std::string getPrismInputFilename() const;
264
271 std::string getJaniInputFilename() const;
272
278 bool isTransitionRewardsSet() const;
279
286 std::string getTransitionRewardsFilename() const;
287
293 bool isStateRewardsSet() const;
294
301 std::string getStateRewardsFilename() const;
302
308 bool isChoiceLabelingSet() const;
309
316 std::string getChoiceLabelingFilename() const;
317
323 bool isConstantsSet() const;
324
330 std::string getConstantDefinitionString() const;
331
336 bool isJaniPropertiesSet() const;
337
342 bool areJaniPropertiesSelected() const;
343
347 std::vector<std::string> getSelectedJaniProperties() const;
348
354 bool isPropertySet() const;
355
361 std::string getProperty() const;
362
368 std::string getPropertyFilter() const;
369
374
379
384
388 bool isQvbsInputSet() const;
389
393 std::string getQvbsModelName() const;
394
398 uint64_t getQvbsInstanceIndex() const;
399
403 boost::optional<std::vector<std::string>> getQvbsPropertyFilter() const;
404
408 std::string getQvbsRoot() const;
409
413 bool isPropertiesAsMultiSet() const;
414
421
426
427 bool check() const override;
428 void finalize() override;
429
430 // The name of the module.
431 static const std::string moduleName;
432
433 private:
434 // Define the string names of the options as constants.
435 static const std::string exportDotOptionName;
436 static const std::string exportDotMaxWidthOptionName;
437 static const std::string exportBuildOptionName;
438 static const std::string exportJaniDotOptionName;
439 static const std::string exportExplicitOptionName;
440 static const std::string exportDdOptionName;
441 static const std::string exportCdfOptionName;
442 static const std::string exportCdfOptionShortName;
443 static const std::string exportSchedulerOptionName;
444 static const std::string exportCheckResultOptionName;
445 static const std::string exportCompressionOptionName;
446 static const std::string exportDigitsOptionName;
447 static const std::string explicitOptionName;
448 static const std::string explicitOptionShortName;
449 static const std::string explicitDrnOptionName;
450 static const std::string explicitDrnOptionShortName;
451 static const std::string explicitUmbOptionName;
452 static const std::string explicitUmbOptionShortName;
453 static const std::string explicitImcaOptionName;
454 static const std::string explicitImcaOptionShortName;
455 static const std::string prismInputOptionName;
456 static const std::string janiInputOptionName;
457 static const std::string prismToJaniOptionName;
458 static const std::string transitionRewardsOptionName;
459 static const std::string stateRewardsOptionName;
460 static const std::string choiceLabelingOptionName;
461 static const std::string constantsOptionName;
462 static const std::string constantsOptionShortName;
463 static const std::string janiPropertyOptionName;
464 static const std::string janiPropertyOptionShortName;
465 static const std::string propertyOptionName;
466 static const std::string propertyOptionShortName;
467 static const std::string steadyStateDistrOptionName;
468 static const std::string expectedVisitingTimesOptionName;
469 static const std::string qvbsInputOptionName;
470 static const std::string qvbsInputOptionShortName;
471 static const std::string qvbsRootOptionName;
472 static const std::string propertiesAsMultiOptionName;
473 static const std::string uncertaintyResolutionModeName;
474};
475
476} // namespace modules
477} // namespace settings
478} // namespace storm
479
480#endif /* STORM_SETTINGS_MODULES_IOSETTINGS_H_ */
bool isJaniPropertiesSet() const
Retrieves whether the jani-property option was set.
UncertaintyResolutionModeSetting getUncertaintyResolutionMode() const
Retrieves the mode deciding how the uncertainty should be resolved.
bool isExportExplicitSet() const
Retrieves whether the export-to-explicit option was set.
std::string getExportExplicitFilename() const
Retrieves the name in which to write the model in explicit format, if the option was set.
std::string getExportBuildFilename() const
Retrieves the name in which to write the model in json format, if export-to-json option was set.
bool isExportCdfSet() const
Retrieves whether the cumulative density function for reward bounded properties should be exported.
static const std::string moduleName
Definition IOSettings.h:431
std::string getExplicitIMCAFilename() const
Retrieves the name of the file that contains the model in the IMCA format.
bool areJaniPropertiesSelected() const
Retrieves whether one or more jani-properties have been selected.
std::string getExportJaniDotFilename() const
Retrieves the name in which to write the jani model in dot format, if the export-to-jani-dot option w...
bool isExportCheckResultSet() const
Retrieves whether the check result should be exported.
std::string getChoiceLabelingFilename() const
Retrieves the name of the file that contains the choice labeling if the model was given using the exp...
bool isStateRewardsSet() const
Retrieves whether the state reward option was set.
bool isExportDdSet() const
Retrieves whether the export-to-dd option was set.
std::string getExportSchedulerFilename() const
Retrieves a filename to which an optimal scheduler will be exported.
std::string getExportCdfDirectory() const
Retrieves a path to a directory in which the cdf files will be stored.
bool isPrismToJaniSet() const
Retrieves whether the option to convert PRISM to JANI input was set.
size_t getExportDotMaxWidth() const
Retrieves the maximal width for labels in the dot format.
std::string getProperty() const
Retrieves the property specified with the property option.
std::string getJaniInputFilename() const
Retrieves the name of the file that contains the JANI model specification if the model was given usin...
bool isExportDotSet() const
Retrieves whether the export-to-dot option was set.
bool isChoiceLabelingSet() const
Retrieves whether the choice labeling option was set.
bool isPrismOrJaniInputSet() const
Retrieves whether the JANI or PRISM input option was set.
std::string getPropertyFilter() const
Retrieves the property filter.
bool isExportBuildSet() const
Retrieves whether the exportbuild option was set.
std::string getPrismInputFilename() const
Retrieves the name of the file that contains the PRISM model specification if the model was given usi...
bool isQvbsInputSet() const
Retrieves whether the input model is to be read from the quantitative verification benchmark set (QVB...
bool isComputeSteadyStateDistributionSet() const
Retrieves whether the steady-state distribution is to be computed.
std::string getConstantDefinitionString() const
Retrieves the string that defines the constants of a symbolic model (given via the symbolic option).
bool isExplicitDRNSet() const
Retrieves whether the explicit option with DRN was set.
std::string getExplicitDRNFilename() const
Retrieves the name of the file that contains the model in the DRN format.
bool isExportDigitsSet() const
Retrieves whether the number of digits for exporting floating point numbers was set.
std::string getLabelingFilename() const
Retrieves the name of the file that contains the state labeling if the model was given using the expl...
void finalize() override
Prepares the modules for further usage, should be called at the end of the initialization,...
boost::optional< std::vector< std::string > > getQvbsPropertyFilter() const
Retrieves the selected property names.
bool isExportSchedulerSet() const
Retrieves whether an optimal scheduler is to be exported.
bool isConstantsSet() const
Retrieves whether the constants option was set.
std::string getStateRewardsFilename() const
Retrieves the name of the file that contains the state rewards if the model was given using the expli...
bool isExplicitUmbSet() const
Retrieves whether the explicit option with UMB was set.
std::string getTransitionRewardsFilename() const
Retrieves the name of the file that contains the transition rewards if the model was given using the ...
bool check() const override
Checks whether the settings are consistent.
bool isPropertySet() const
Retrieves whether the property option was set.
std::string getQvbsModelName() const
Retrieves the specified model (short-)name of the QVBS.
std::vector< std::string > getSelectedJaniProperties() const
storm::io::CompressionMode getCompressionMode() const
Retrieves the preferred compression mode.
IOSettings()
Creates a new set of IO settings.
std::string getExportCheckResultFilename() const
Retrieves a filename to which the check result should be exported.
storm::SteadyStateDistributionAlgorithm getSteadyStateDistributionAlgorithm() const
std::string getTransitionFilename() const
Retrieves the name of the file that contains the transitions if the model was given using the explici...
bool isJaniInputSet() const
Retrieves whether the JANI input option was set.
size_t getExportDigits() const
Retrieves the number of digits for exporting floating point numbers.
uint64_t getQvbsInstanceIndex() const
Retrieves the selected model instance (file + open parameters of the model).
bool isExplicitIMCASet() const
Retrieves whether the explicit option with IMCA was set.
bool isExplicitExportPlaceholdersDisabled() const
Retrieves whether we prevent the usage of placeholders in the explicit DRN format.
std::string getExportDotFilename() const
Retrieves the name in which to write the model in dot format, if the export-to-dot option was set.
storm::io::ModelExportFormat getExportBuildFormat() const
Retrieves the specified export format for the exportbuild option.
bool isPropertiesAsMultiSet() const
Retrieves whether the input properties are to be interpreted as a single multi-objective formula.
bool isCompressionSet() const
Retrieves whether a preferred compression mode has been set.
std::string getQvbsRoot() const
Retrieves the specified root directory of qvbs.
bool isPrismInputSet() const
Retrieves whether the PRISM language option was set.
bool isComputeExpectedVisitingTimesSet() const
Retrieves whether the expected visiting times are to be computed.
bool isTransitionRewardsSet() const
Retrieves whether the transition reward option was set.
std::string getExplicitUmbFilename() const
Retrieves the name of the file that contains the model in the UMB format.
bool isExplicitSet() const
Retrieves whether the explicit option was set.
std::string getExportDdFilename() const
Retrieves the name in which to write the model in dd format, if the option was set.
bool isExportJaniDotSet() const
Retrieves whether the export-to-dot option for jani was set.
ModuleSettings(std::string const &moduleName)
Constructs a new settings object.
solver::UncertaintyResolutionModeSetting UncertaintyResolutionModeSetting