Storm 1.11.1.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"
12
13namespace storm {
14namespace settings {
15namespace modules {
16
20class IOSettings : public ModuleSettings {
21 public:
25 IOSettings();
26
32 bool isExportDotSet() const;
33
39 std::string getExportDotFilename() const;
40
46 size_t getExportDotMaxWidth() const;
47
51 bool isExportBuildSet() const;
52
56 std::string getExportBuildFilename() const;
57
62
68 bool isExportJaniDotSet() const;
69
75 std::string getExportJaniDotFilename() const;
76
82 bool isExportExplicitSet() const;
83
89 std::string getExportExplicitFilename() const;
90
96 bool isExportDdSet() const;
97
103 std::string getExportDdFilename() const;
104
108 bool isExportCdfSet() const;
109
113 std::string getExportCdfDirectory() const;
114
118 bool isExportSchedulerSet() const;
119
123 std::string getExportSchedulerFilename() const;
124
128 bool isExportCheckResultSet() const;
129
133 std::string getExportCheckResultFilename() const;
134
140 bool isExplicitSet() const;
141
148 std::string getTransitionFilename() const;
149
156 std::string getLabelingFilename() const;
157
163 bool isExplicitDRNSet() const;
164
170 std::string getExplicitDRNFilename() const;
171
177
183 bool isExplicitIMCASet() const;
184
190 std::string getExplicitIMCAFilename() const;
191
197 bool isPrismInputSet() const;
198
204 bool isJaniInputSet() const;
205
211 bool isPrismOrJaniInputSet() const;
212
218 bool isPrismToJaniSet() const;
219
226 std::string getPrismInputFilename() const;
227
234 std::string getJaniInputFilename() const;
235
241 bool isTransitionRewardsSet() const;
242
249 std::string getTransitionRewardsFilename() const;
250
256 bool isStateRewardsSet() const;
257
264 std::string getStateRewardsFilename() const;
265
271 bool isChoiceLabelingSet() const;
272
279 std::string getChoiceLabelingFilename() const;
280
286 bool isConstantsSet() const;
287
293 std::string getConstantDefinitionString() const;
294
299 bool isJaniPropertiesSet() const;
300
305 bool areJaniPropertiesSelected() const;
306
310 std::vector<std::string> getSelectedJaniProperties() const;
311
317 bool isPropertySet() const;
318
324 std::string getProperty() const;
325
331 std::string getPropertyFilter() const;
332
337
342
347
351 bool isQvbsInputSet() const;
352
356 std::string getQvbsModelName() const;
357
361 uint64_t getQvbsInstanceIndex() const;
362
366 boost::optional<std::vector<std::string>> getQvbsPropertyFilter() const;
367
371 std::string getQvbsRoot() const;
372
376 bool isPropertiesAsMultiSet() const;
377
384
389
390 bool check() const override;
391 void finalize() override;
392
393 // The name of the module.
394 static const std::string moduleName;
395
396 private:
397 // Define the string names of the options as constants.
398 static const std::string exportDotOptionName;
399 static const std::string exportDotMaxWidthOptionName;
400 static const std::string exportBuildOptionName;
401 static const std::string exportJaniDotOptionName;
402 static const std::string exportExplicitOptionName;
403 static const std::string exportDdOptionName;
404 static const std::string exportCdfOptionName;
405 static const std::string exportCdfOptionShortName;
406 static const std::string exportSchedulerOptionName;
407 static const std::string exportCheckResultOptionName;
408 static const std::string explicitOptionName;
409 static const std::string explicitOptionShortName;
410 static const std::string explicitDrnOptionName;
411 static const std::string explicitDrnOptionShortName;
412 static const std::string explicitImcaOptionName;
413 static const std::string explicitImcaOptionShortName;
414 static const std::string prismInputOptionName;
415 static const std::string janiInputOptionName;
416 static const std::string prismToJaniOptionName;
417 static const std::string transitionRewardsOptionName;
418 static const std::string stateRewardsOptionName;
419 static const std::string choiceLabelingOptionName;
420 static const std::string constantsOptionName;
421 static const std::string constantsOptionShortName;
422 static const std::string janiPropertyOptionName;
423 static const std::string janiPropertyOptionShortName;
424 static const std::string propertyOptionName;
425 static const std::string propertyOptionShortName;
426 static const std::string steadyStateDistrOptionName;
427 static const std::string expectedVisitingTimesOptionName;
428 static const std::string qvbsInputOptionName;
429 static const std::string qvbsInputOptionShortName;
430 static const std::string qvbsRootOptionName;
431 static const std::string propertiesAsMultiOptionName;
432 static const std::string uncertaintyResolutionModeName;
433};
434
435} // namespace modules
436} // namespace settings
437} // namespace storm
438
439#endif /* STORM_SETTINGS_MODULES_IOSETTINGS_H_ */
This class represents the markov chain settings.
Definition IOSettings.h:20
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:394
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.
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...
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
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.
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.
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.
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.
This is the base class of the settings for a particular module.