Storm
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"
11
12namespace storm {
13namespace settings {
14namespace modules {
15
19class IOSettings : public ModuleSettings {
20 public:
24 IOSettings();
25
31 bool isExportDotSet() const;
32
38 std::string getExportDotFilename() const;
39
45 size_t getExportDotMaxWidth() const;
46
50 bool isExportBuildSet() const;
51
55 std::string getExportBuildFilename() const;
56
61
67 bool isExportJaniDotSet() const;
68
74 std::string getExportJaniDotFilename() const;
75
81 bool isExportExplicitSet() const;
82
88 std::string getExportExplicitFilename() const;
89
95 bool isExportDdSet() const;
96
102 std::string getExportDdFilename() const;
103
107 bool isExportCdfSet() const;
108
112 std::string getExportCdfDirectory() const;
113
117 bool isExportSchedulerSet() const;
118
122 std::string getExportSchedulerFilename() const;
123
127 bool isExportCheckResultSet() const;
128
132 std::string getExportCheckResultFilename() const;
133
139 bool isExplicitSet() const;
140
147 std::string getTransitionFilename() const;
148
155 std::string getLabelingFilename() const;
156
162 bool isExplicitDRNSet() const;
163
169 std::string getExplicitDRNFilename() const;
170
176
182 bool isExplicitIMCASet() const;
183
189 std::string getExplicitIMCAFilename() const;
190
196 bool isPrismInputSet() const;
197
203 bool isJaniInputSet() const;
204
210 bool isPrismOrJaniInputSet() const;
211
217 bool isPrismToJaniSet() const;
218
225 std::string getPrismInputFilename() const;
226
233 std::string getJaniInputFilename() const;
234
240 bool isTransitionRewardsSet() const;
241
248 std::string getTransitionRewardsFilename() const;
249
255 bool isStateRewardsSet() const;
256
263 std::string getStateRewardsFilename() const;
264
270 bool isChoiceLabelingSet() const;
271
278 std::string getChoiceLabelingFilename() const;
279
285 bool isConstantsSet() const;
286
292 std::string getConstantDefinitionString() const;
293
298 bool isJaniPropertiesSet() const;
299
304 bool areJaniPropertiesSelected() const;
305
309 std::vector<std::string> getSelectedJaniProperties() const;
310
316 bool isPropertySet() const;
317
323 std::string getProperty() const;
324
330 std::string getPropertyFilter() const;
331
336
341
346
350 bool isQvbsInputSet() const;
351
355 std::string getQvbsModelName() const;
356
361
365 boost::optional<std::vector<std::string>> getQvbsPropertyFilter() const;
366
370 std::string getQvbsRoot() const;
371
375 bool isPropertiesAsMultiSet() const;
376
377 bool check() const override;
378 void finalize() override;
379
380 // The name of the module.
381 static const std::string moduleName;
382
383 private:
384 // Define the string names of the options as constants.
385 static const std::string exportDotOptionName;
386 static const std::string exportDotMaxWidthOptionName;
387 static const std::string exportBuildOptionName;
388 static const std::string exportJaniDotOptionName;
389 static const std::string exportExplicitOptionName;
390 static const std::string exportDdOptionName;
391 static const std::string exportCdfOptionName;
392 static const std::string exportCdfOptionShortName;
393 static const std::string exportSchedulerOptionName;
394 static const std::string exportCheckResultOptionName;
395 static const std::string explicitOptionName;
396 static const std::string explicitOptionShortName;
397 static const std::string explicitDrnOptionName;
398 static const std::string explicitDrnOptionShortName;
399 static const std::string explicitImcaOptionName;
400 static const std::string explicitImcaOptionShortName;
401 static const std::string prismInputOptionName;
402 static const std::string janiInputOptionName;
403 static const std::string prismToJaniOptionName;
404 static const std::string transitionRewardsOptionName;
405 static const std::string stateRewardsOptionName;
406 static const std::string choiceLabelingOptionName;
407 static const std::string constantsOptionName;
408 static const std::string constantsOptionShortName;
409 static const std::string janiPropertyOptionName;
410 static const std::string janiPropertyOptionShortName;
411 static const std::string propertyOptionName;
412 static const std::string propertyOptionShortName;
413 static const std::string steadyStateDistrOptionName;
414 static const std::string expectedVisitingTimesOptionName;
415 static const std::string qvbsInputOptionName;
416 static const std::string qvbsInputOptionShortName;
417 static const std::string qvbsRootOptionName;
418 static const std::string propertiesAsMultiOptionName;
419};
420
421} // namespace modules
422} // namespace settings
423} // namespace storm
424
425#endif /* STORM_SETTINGS_MODULES_IOSETTINGS_H_ */
This class represents the markov chain settings.
Definition IOSettings.h:19
bool isJaniPropertiesSet() const
Retrieves whether the jani-property option was set.
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:381
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.
SettingsType const & getModule()
Get module.
LabParser.cpp.
Definition cli.cpp:18