Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DftIOSettings.h
Go to the documentation of this file.
1#pragma once
2
4
5namespace storm::dft {
6namespace settings {
7namespace modules {
8
13 public:
18
24 bool isDftFileSet() const;
25
31 std::string getDftFilename() const;
32
38 bool isDftJsonFileSet() const;
39
45 std::string getDftJsonFilename() const;
46
52 bool usePropExpectedTime() const;
53
59 bool usePropProbability() const;
60
66 bool usePropTimebound() const;
67
73 double getPropTimebound() const;
74
80 bool usePropTimepoints() const;
81
87 std::vector<double> getPropTimepoints() const;
88
94 bool isComputeMinimalValue() const;
95
101 bool isComputeMaximalValue() const;
102
108 bool isExportToJson() const;
109
115 bool isExportToSmt() const;
116
122 bool isAnalyzeWithBdds() const;
123
129 bool isMinimalCutSets() const;
130
136 bool isExportToBddDot() const;
137
143 std::string getExportJsonFilename() const;
144
150 std::string getExportSmtFilename() const;
151
157 std::string getExportBddDotFilename() const;
158
164 bool isShowDftStatisticsSet() const;
165
171 bool isImportanceMeasureSet() const;
172
178 std::string getImportanceMeasure() const;
179
185 bool isVariableOrderingFileSet() const;
186
192 std::string getVariableOrderingFilename() const;
193
194 bool check() const override;
195 void finalize() override;
196
197 // The name of the module.
198 static const std::string moduleName;
199
200 private:
201 // Define the string names of the options as constants.
202 static const std::string dftFileOptionName;
203 static const std::string dftFileOptionShortName;
204 static const std::string dftJsonFileOptionName;
205 static const std::string dftJsonFileOptionShortName;
206 static const std::string propExpectedTimeOptionName;
207 static const std::string propExpectedTimeOptionShortName;
208 static const std::string propProbabilityOptionName;
209 static const std::string propTimeboundOptionName;
210 static const std::string propTimepointsOptionName;
211 static const std::string minValueOptionName;
212 static const std::string maxValueOptionName;
213 static const std::string analyzeWithBdds;
214 static const std::string minimalCutSets;
215 static const std::string exportToJsonOptionName;
216 static const std::string exportToSmtOptionName;
217 static const std::string exportToBddDotOptionName;
218 static const std::string dftStatisticsOptionName;
219 static const std::string dftStatisticsOptionShortName;
220 static const std::string importanceMeasureOptionName;
221 static const std::string variableOrderingFileOptionName;
222};
223
224} // namespace modules
225} // namespace settings
226} // namespace storm::dft
This class represents the settings for IO operations concerning DFTs.
bool usePropTimepoints() const
Retrieves whether the property timepoints should be used.
void finalize() override
Prepares the modules for further usage, should be called at the end of the initialization,...
DftIOSettings()
Creates a new set of IO settings for DFTs.
bool usePropTimebound() const
Retrieves whether the property timebound should be used.
bool usePropExpectedTime() const
Retrieves whether the property expected time should be used.
bool isDftFileSet() const
Retrieves whether the dft file option was set.
std::string getDftJsonFilename() const
Retrieves the name of the json file that contains the dft specification.
bool isAnalyzeWithBdds() const
Retrieves whether the analyze with Bdds option was set.
bool isMinimalCutSets() const
Retrieves whether the minimal cut sets option was set.
double getPropTimebound() const
Retrieves the timebound for the timebound property.
std::string getVariableOrderingFilename() const
Retrieves the name of the file that contains the variable ordering.
bool usePropProbability() const
Retrieves whether the property probability should be used.
bool isComputeMaximalValue() const
Retrieves whether the maximal value should be computed for non-determinism.
bool isShowDftStatisticsSet() const
Retrieves whether statistics about the DFT analysis should be displayed.
bool isExportToSmt() const
Retrieves whether the export to smtlib2 file option was set.
bool isDftJsonFileSet() const
Retrieves whether the dft file option for Json was set.
bool isVariableOrderingFileSet() const
Retrieves whether the varialble ordering file option was set.
std::string getExportSmtFilename() const
Retrieves the name of the smtlib2 file to export to.
bool isExportToJson() const
Retrieves whether the export to Json file option was set.
std::string getDftFilename() const
Retrieves the name of the file that contains the dft specification.
bool isImportanceMeasureSet() const
Retrieves whether to calculate an importance measure.
bool isComputeMinimalValue() const
Retrieves whether the minimal value should be computed for non-determinism.
bool check() const override
Checks whether the settings are consistent.
std::string getImportanceMeasure() const
Retrieves the name of the importance measure to calculate.
std::vector< double > getPropTimepoints() const
Retrieves the settings for the timepoints property.
std::string getExportBddDotFilename() const
Retrieves the name of the dot file to export to.
bool isExportToBddDot() const
Retrieves whether the export to Bdd Dot file option was set.
std::string getExportJsonFilename() const
Retrieves the name of the json file to export to.
This is the base class of the settings for a particular module.