Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DFTGalileoParser.cpp
Go to the documentation of this file.
2
3#include <boost/algorithm/string.hpp>
4#include <optional>
5#include <regex>
6
14#include "storm/io/file.h"
16
17namespace storm::dft {
18namespace parser {
19
20template<typename ValueType>
24 // Regular expression to detect comments
25 // taken from: https://stackoverflow.com/questions/9449887/removing-c-c-style-comments-using-boostregex
26 const std::regex commentRegex("(/\\*([^*]|(\\*+[^*/]))*\\*+/)|(//.*)");
27
28 std::ifstream file;
29 storm::io::openFile(filename, file);
30
31 std::string line;
32 size_t lineNo = 0;
33 std::string toplevelId = "";
34 bool comment = false; // Indicates whether the current line is part of a multiline comment
35 try {
36 while (storm::io::getline(file, line)) {
37 ++lineNo;
38 // First consider comments
39 if (comment) {
40 // Line is part of multiline comment -> search for end of this comment
41 size_t commentEnd = line.find("*/");
42 if (commentEnd == std::string::npos) {
43 continue;
44 } else {
45 // Remove comment
46 line = line.substr(commentEnd + 2);
47 comment = false;
48 }
49 }
50 // Remove in-line comments
51 line = std::regex_replace(line, commentRegex, "");
52 // Check if multiline comment starts
53 size_t commentStart = line.find("/*");
54 if (commentStart != std::string::npos) {
55 // Only keep part before comment
56 line = line.substr(0, commentStart);
57 comment = true;
58 }
59
60 boost::trim(line);
61 if (line.empty()) {
62 // Empty line
63 continue;
64 }
65
66 // Remove semicolon
67 STORM_LOG_THROW(line.back() == ';', storm::exceptions::WrongFormatException, "Semicolon expected at the end of line " << lineNo << ".");
68 line.pop_back();
69
70 // Split line into tokens w.r.t. white space
71 boost::trim(line);
72 std::vector<std::string> tokens;
73 boost::split(tokens, line, boost::is_any_of(" \t"), boost::token_compress_on);
74
75 // Start actual parsing
76 if (tokens[0] == "toplevel") {
77 // Top level indicator
78 STORM_LOG_THROW(toplevelId.empty(), storm::exceptions::WrongFormatException, "Toplevel element already defined.");
79 STORM_LOG_THROW(tokens.size() == 2, storm::exceptions::WrongFormatException, "Expected unique element id after 'toplevel'.");
80 toplevelId = parseName(tokens[1]);
81 } else if (tokens[0] == "param") {
82 // Parameters
83 STORM_LOG_THROW(tokens.size() == 2, storm::exceptions::WrongFormatException, "Expected unique parameter name after 'param'.");
84 STORM_LOG_THROW((std::is_same<ValueType, storm::RationalFunction>::value), storm::exceptions::NotSupportedException,
85 "Parameters are only allowed when using rational functions.");
86 valueParser.addParameter(parseName(tokens[1]));
87 } else {
88 // DFT element
89 std::string name = parseName(tokens[0]);
90
91 std::vector<std::string> childNames;
92 for (size_t i = 2; i < tokens.size(); ++i) {
93 childNames.push_back(parseName(tokens[i]));
94 }
95
96 // Add element according to type
97 std::string type = tokens[1];
98 if (type == "and") {
99 builder.addAndGate(name, childNames);
100 } else if (type == "or") {
101 builder.addOrGate(name, childNames);
102 } else if (boost::starts_with(type, "vot")) {
103 size_t threshold = storm::parser::parseNumber<size_t>(type.substr(3));
104 builder.addVotingGate(name, threshold, childNames);
105 } else if (type.find("of") != std::string::npos) {
106 size_t pos = type.find("of");
107 size_t threshold = storm::parser::parseNumber<size_t>(type.substr(0, pos));
108 size_t count = storm::parser::parseNumber<size_t>(type.substr(pos + 2));
109 STORM_LOG_THROW(count == childNames.size(), storm::exceptions::WrongFormatException,
110 "Voting gate number " << count << " does not correspond to number of children " << childNames.size() << ".");
111 builder.addVotingGate(name, threshold, childNames);
112 } else if (type == "pand") {
113 builder.addPandGate(name, childNames);
114 } else if (type == "pand-incl" || type == "pand<=") {
115 builder.addPandGate(name, childNames, true);
116 } else if (type == "pand-excl" || type == "pand<") {
117 builder.addPandGate(name, childNames, false);
118 } else if (type == "por") {
119 builder.addPorGate(name, childNames);
120 } else if (type == "por-incl" || type == "por<=") {
121 builder.addPorGate(name, childNames, true);
122 } else if (type == "por-excl" || type == "por<") {
123 builder.addPorGate(name, childNames, false);
124 } else if (type == "wsp" || type == "csp" || type == "hsp" || type == "spare") {
125 builder.addSpareGate(name, childNames);
126 } else if (type == "seq") {
127 builder.addSequenceEnforcer(name, childNames);
128 } else if (type == "mutex") {
129 builder.addMutex(name, childNames);
130 } else if (type == "fdep") {
131 builder.addPdep(name, childNames, storm::utility::one<ValueType>());
132 } else if (boost::starts_with(type, "pdep=")) {
133 ValueType probability = valueParser.parseValue(type.substr(5));
134 builder.addPdep(name, childNames, probability);
135 } else if (type.find("=") != std::string::npos) {
136 // Use dedicated method for parsing BEs
137 // Remove name from line and parse remainder
138 std::regex regexName("\"?" + tokens[0] + "\"?");
139 std::string remaining_line = std::regex_replace(line, regexName, "");
140 parseBasicElement(name, remaining_line, builder, valueParser);
141 } else if (type.find("insp") != std::string::npos) {
142 // Inspection as defined by DFTCalc
143 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Inspections are not supported.");
144 } else {
145 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name '" << type << "' not recognized.");
146 }
147 }
148 }
149 } catch (storm::exceptions::BaseException const& exception) {
150 STORM_LOG_THROW(false, storm::exceptions::FileIoException, "A parsing exception occurred in line " << lineNo << ": " << exception.what() << ".");
151 }
152 builder.setTopLevel(toplevelId);
154
155 // Build DFT
156 return builder.build();
157}
158
159template<typename ValueType>
160std::string DFTGalileoParser<ValueType>::parseName(std::string const& name) {
161 size_t firstQuots = name.find("\"");
162 if (firstQuots != std::string::npos) {
163 // Remove quotation marks
164 size_t secondQuots = name.find("\"", firstQuots + 1);
165 STORM_LOG_THROW(secondQuots != std::string::npos, storm::exceptions::WrongFormatException, "No ending quotation mark found in " << name << ".");
166 return name.substr(firstQuots + 1, secondQuots - 1);
167 } else {
168 return name;
169 }
170}
171
172template<typename ValueType>
173std::string DFTGalileoParser<ValueType>::parseValue(std::string name, std::string& line) {
174 // Build regex for: name=(value)
175 std::regex nameRegex(name + "\\s*=\\s*([^\\s]*)");
176 std::smatch match;
177 if (std::regex_search(line, match, nameRegex)) {
178 // Remove matched part
179 std::string value = match.str(1);
180 line = std::regex_replace(line, nameRegex, "");
181 return value;
182 } else {
183 // No match found
184 return "";
185 }
186}
187
188template<typename ValueType>
189void DFTGalileoParser<ValueType>::parseBasicElement(std::string const& name, std::string& input, storm::dft::builder::DFTBuilder<ValueType>& builder,
191 // Avoid writing too much
192 using namespace storm::dft::storage::elements;
193
194 // Parameters for distributions
195 std::optional<BEType> distribution;
196 std::optional<ValueType> prob;
197 std::optional<ValueType> lambda;
198 std::optional<size_t> phases;
199 std::optional<ValueType> shape;
200 std::optional<ValueType> rate;
201 std::optional<ValueType> mean;
202 std::optional<ValueType> stddev;
203 std::optional<ValueType> dorm;
204
205 // Parse distribution parameters
206 // Constant distribution
207 std::string value = parseValue("prob", input);
208 if (!value.empty()) {
209 prob = valueParser.parseValue(value);
210 distribution = BEType::PROBABILITY;
211 }
212
213 // Exponential distribution
214 value = parseValue("lambda", input);
215 if (!value.empty()) {
217 !distribution.has_value(), storm::exceptions::WrongFormatException,
218 "Two distributions " << toString(distribution.value()) << " and " << toString(BEType::EXPONENTIAL) << " are defined for BE '" << name << "'.");
219 lambda = valueParser.parseValue(value);
220 distribution = BEType::EXPONENTIAL;
221 }
222
223 // Erlang distribution
224 // Parameter 'lambda' was already handled before for exponential distribution
225 value = parseValue("phases", input);
226 if (!value.empty()) {
228 !distribution.has_value() || distribution.value() == BEType::EXPONENTIAL, storm::exceptions::WrongFormatException,
229 "Two distributions " << toString(distribution.value()) << " and " << toString(BEType::ERLANG) << " are defined for BE '" << name << "'.");
231 distribution = BEType::ERLANG;
232 }
233
234 // Weibull distribution
235 value = parseValue("shape", input);
236 if (!value.empty()) {
238 !distribution.has_value(), storm::exceptions::WrongFormatException,
239 "Two distributions " << toString(distribution.value()) << " and " << toString(BEType::WEIBULL) << " are defined for BE '" << name << "'.");
240 shape = valueParser.parseValue(value);
241 distribution = BEType::WEIBULL;
242 }
243 value = parseValue("rate", input);
244 if (!value.empty()) {
246 !distribution.has_value() || distribution.value() == BEType::WEIBULL, storm::exceptions::WrongFormatException,
247 "Two distributions " << toString(distribution.value()) << " and " << toString(BEType::WEIBULL) << " are defined for BE '" << name << "'.");
248 rate = valueParser.parseValue(value);
249 }
250
251 // Log-normal distribution
252 value = parseValue("mean", input);
253 if (!value.empty()) {
255 !distribution.has_value(), storm::exceptions::WrongFormatException,
256 "Two distributions " << toString(distribution.value()) << " and " << toString(BEType::LOGNORMAL) << " are defined for BE '" << name << "'.");
257 mean = valueParser.parseValue(value);
258 distribution = BEType::LOGNORMAL;
259 }
260 value = parseValue("stddev", input);
261 if (!value.empty()) {
263 !distribution.has_value() || distribution.value() == BEType::LOGNORMAL, storm::exceptions::WrongFormatException,
264 "Two distributions " << toString(distribution.value()) << " and " << toString(BEType::LOGNORMAL) << " are defined for BE '" << name << "'.");
265 stddev = valueParser.parseValue(value);
266 }
267
268 // Dormancy factor
269 value = parseValue("dorm", input);
270 if (!value.empty()) {
271 dorm = valueParser.parseValue(value);
272 }
273
274 // Additional arguments (wich are not supported)
275 value = parseValue("cov", input);
276 if (!value.empty()) {
277 STORM_LOG_WARN("Coverage is not supported and will be ignored for basic element '" << name << "'.");
278 }
279 value = parseValue("res", input);
280 if (!value.empty()) {
281 STORM_LOG_WARN("Restoration is not supported and will be ignored for basic element '" << name << "'.");
282 }
283 value = parseValue("repl", input);
284 if (!value.empty()) {
285 size_t replication = storm::parser::parseNumber<size_t>(value);
286 STORM_LOG_THROW(replication == 1, storm::exceptions::NotSupportedException, "Replication > 1 is not supported for basic element '" << name << "'.");
287 }
288 value = parseValue("interval", input);
289 if (!value.empty()) {
290 STORM_LOG_WARN("Interval is not supported and will be ignored for basic element '" << name << "'.");
291 }
292 value = parseValue("repair", input);
293 STORM_LOG_THROW(value.empty(), storm::exceptions::NotSupportedException,
294 "Repairs are not supported and will be ignored for basic element '" << name << "'.");
295
296 boost::trim(input);
297 STORM_LOG_THROW(input == "", storm::exceptions::WrongFormatException, "Unknown arguments for basic element '" << name << "': " << input << ".");
298
299 // Create BE with given distribution
300 STORM_LOG_THROW(distribution.has_value(), storm::exceptions::WrongFormatException, "No failure distribution is defined for BE '" << name << "'.");
301 switch (distribution.value()) {
302 case BEType::PROBABILITY:
303 STORM_LOG_THROW(prob.has_value(), storm::exceptions::WrongFormatException,
304 "Distribution " << toString(BEType::PROBABILITY) << " requires parameter 'prob' for BE '" << name << "'.");
305 if (!dorm.has_value()) {
306 STORM_LOG_WARN("No dormancy factor was provided for basic element '" << name << "'. Assuming dormancy factor of 1.");
308 }
309 builder.addBasicElementProbability(name, prob.value(), dorm.value());
310 break;
311 case BEType::EXPONENTIAL:
312 STORM_LOG_THROW(lambda.has_value(), storm::exceptions::WrongFormatException,
313 "Distribution " << toString(BEType::EXPONENTIAL) << " requires parameter 'lambda' for BE '" << name << "'.");
314 if (!dorm.has_value()) {
315 STORM_LOG_WARN("No dormancy factor was provided for basic element '" << name << "'. Assuming dormancy factor of 1.");
317 }
318 builder.addBasicElementExponential(name, lambda.value(), dorm.value());
319 break;
320 case BEType::ERLANG:
321 STORM_LOG_THROW(lambda.has_value(), storm::exceptions::WrongFormatException,
322 "Distribution " << toString(BEType::ERLANG) << " requires parameter 'lambda' for BE '" << name << "'.");
323 STORM_LOG_THROW(phases.has_value(), storm::exceptions::WrongFormatException,
324 "Distribution " << toString(BEType::ERLANG) << " requires parameter 'phases' for BE '" << name << "'.");
325 if (!dorm.has_value()) {
326 STORM_LOG_WARN("No dormancy factor was provided for basic element '" << name << "'. Assuming dormancy factor of 1.");
328 }
329 builder.addBasicElementErlang(name, lambda.value(), phases.value(), dorm.value());
330 break;
331 case BEType::WEIBULL:
332 STORM_LOG_THROW(shape.has_value(), storm::exceptions::WrongFormatException,
333 "Distribution " << toString(BEType::WEIBULL) << " requires parameter 'shape' for BE '" << name << "'.");
334 STORM_LOG_THROW(rate.has_value(), storm::exceptions::WrongFormatException,
335 "Distribution " << toString(BEType::WEIBULL) << " requires parameter 'rate' for BE '" << name << "'.");
336 builder.addBasicElementWeibull(name, shape.value(), rate.value());
337 break;
338 case BEType::LOGNORMAL:
339 STORM_LOG_THROW(mean.has_value(), storm::exceptions::WrongFormatException,
340 "Distribution " << toString(BEType::LOGNORMAL) << " requires parameter 'mean' for BE '" << name << "'.");
341 STORM_LOG_THROW(stddev.has_value(), storm::exceptions::WrongFormatException,
342 "Distribution " << toString(BEType::WEIBULL) << " requires parameter 'stddev' for BE '" << name << "'.");
343 builder.addBasicElementLogNormal(name, mean.value(), stddev.value());
344 break;
345 default:
346 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "No distribution defined for basic element '" << name << "'.");
347 break;
348 }
349}
350
351// Explicitly instantiate the class.
352template class DFTGalileoParser<double>;
354
355} // namespace parser
356} // namespace storm::dft
void addBasicElementErlang(std::string const &name, ValueType rate, unsigned phases, ValueType dormancyFactor)
Create BE with Erlang distribution and add it to DFT.
void addBasicElementProbability(std::string const &name, ValueType probability, ValueType dormancyFactor)
Create BE with constant (Bernoulli) distribution and add it to DFT.
void addBasicElementExponential(std::string const &name, ValueType rate, ValueType dormancyFactor, bool transient=false)
Create BE with exponential distribution and add it to DFT.
void addBasicElementWeibull(std::string const &name, ValueType shape, ValueType rate)
Create BE with Weibull distribution and add it to DFT.
void addBasicElementLogNormal(std::string const &name, ValueType mean, ValueType standardDeviation)
Create BE with log-normal distribution and add it to DFT.
Parser for DFT in the Galileo format.
static storm::dft::storage::DFT< ValueType > parseDFT(std::string const &filename)
Parse DFT in Galileo format and build DFT.
static std::string parseName(std::string const &name)
Parse element name (strip quotation marks, etc.).
Represents a Dynamic Fault Tree.
Definition DFT.h:49
This class represents the base class of all exception classes.
virtual const char * what() const noexcept override
Retrieves the message associated with this exception.
Parser for values according to their ValueType.
Definition ValueParser.h:23
void addParameter(std::string const &parameter)
Add declaration of parameter.
ValueType parseValue(std::string const &value) const
Parse ValueType from string.
#define STORM_LOG_WARN(message)
Definition logging.h:28
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:28
std::string toString(DFTElementType const &type)
std::basic_istream< CharT, Traits > & getline(std::basic_istream< CharT, Traits > &input, std::basic_string< CharT, Traits, Allocator > &str)
Overloaded getline function which handles different types of newline ( and \r).
Definition file.h:80
void closeFile(std::ofstream &stream)
Close the given file after writing.
Definition file.h:47
void openFile(std::string const &filepath, std::ofstream &filestream, bool append=false, bool silent=false)
Open the given file for writing.
Definition file.h:18
ValueType parseValue(std::string const &valueStr, std::unordered_map< std::string, ValueType > const &placeholders, ValueParser< ValueType > const &valueParser)
NumberType parseNumber(std::string const &value)
Parse number from string.
ValueType one()
Definition constants.cpp:19