Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DFTGalileoParser.cpp
Go to the documentation of this file.
1#include "DFTGalileoParser.h"
2
3#include <boost/algorithm/string.hpp>
4#include <boost/algorithm/string/replace.hpp>
5#include <optional>
6#include <regex>
7
11#include "storm/io/file.h"
13
14namespace storm::dft {
15namespace parser {
16
17template<typename ValueType>
21 // Regular expression to detect comments
22 // taken from: https://stackoverflow.com/questions/9449887/removing-c-c-style-comments-using-boostregex
23 const std::regex commentRegex("(/\\*([^*]|(\\*+[^*/]))*\\*+/)|(//.*)");
24
25 std::ifstream file;
26 storm::io::openFile(filename, file);
27
28 std::string line;
29 size_t lineNo = 0;
30 std::string toplevelId = "";
31 bool comment = false; // Indicates whether the current line is part of a multiline comment
32 try {
33 while (storm::io::getline(file, line)) {
34 ++lineNo;
35 // First consider comments
36 if (comment) {
37 // Line is part of multiline comment -> search for end of this comment
38 size_t commentEnd = line.find("*/");
39 if (commentEnd == std::string::npos) {
40 continue;
41 } else {
42 // Remove comment
43 line = line.substr(commentEnd + 2);
44 comment = false;
45 }
46 }
47 // Remove in-line comments
48 line = std::regex_replace(line, commentRegex, "");
49 // Check if multiline comment starts
50 size_t commentStart = line.find("/*");
51 if (commentStart != std::string::npos) {
52 // Only keep part before comment
53 line = line.substr(0, commentStart);
54 comment = true;
55 }
56
57 boost::trim(line);
58 if (line.empty()) {
59 // Empty line
60 continue;
61 }
62
63 // Remove semicolon
64 STORM_LOG_THROW(line.back() == ';', storm::exceptions::WrongFormatException, "Semicolon expected at the end of line " << lineNo << ".");
65 line.pop_back();
66
67 // Split line into tokens w.r.t. white space
68 boost::trim(line);
69 std::vector<std::string> tokens;
70 boost::split(tokens, line, boost::is_any_of(" \t"), boost::token_compress_on);
71
72 // Start actual parsing
73 if (tokens[0] == "toplevel") {
74 // Top level indicator
75 STORM_LOG_THROW(toplevelId.empty(), storm::exceptions::WrongFormatException, "Toplevel element already defined.");
76 STORM_LOG_THROW(tokens.size() == 2, storm::exceptions::WrongFormatException, "Expected unique element id after 'toplevel'.");
77 toplevelId = parseName(tokens[1]);
78 } else if (tokens[0] == "param") {
79 // Parameters
80 STORM_LOG_THROW(tokens.size() == 2, storm::exceptions::WrongFormatException, "Expected unique parameter name after 'param'.");
81 STORM_LOG_THROW((std::is_same<ValueType, storm::RationalFunction>::value), storm::exceptions::NotSupportedException,
82 "Parameters are only allowed when using rational functions.");
83 valueParser.addParameter(parseName(tokens[1]));
84 } else {
85 // DFT element
86 std::string name = parseName(tokens[0]);
87
88 std::vector<std::string> childNames;
89 for (size_t i = 2; i < tokens.size(); ++i) {
90 childNames.push_back(parseName(tokens[i]));
91 }
92
93 // Add element according to type
94 std::string type = tokens[1];
95 if (type == "and") {
96 builder.addAndGate(name, childNames);
97 } else if (type == "or") {
98 builder.addOrGate(name, childNames);
99 } else if (boost::starts_with(type, "vot")) {
100 size_t threshold = storm::parser::parseNumber<size_t>(type.substr(3));
101 builder.addVotingGate(name, threshold, childNames);
102 } else if (type.find("of") != std::string::npos) {
103 size_t pos = type.find("of");
104 size_t threshold = storm::parser::parseNumber<size_t>(type.substr(0, pos));
105 size_t count = storm::parser::parseNumber<size_t>(type.substr(pos + 2));
106 STORM_LOG_THROW(count == childNames.size(), storm::exceptions::WrongFormatException,
107 "Voting gate number " << count << " does not correspond to number of children " << childNames.size() << ".");
108 builder.addVotingGate(name, threshold, childNames);
109 } else if (type == "pand") {
110 builder.addPandGate(name, childNames);
111 } else if (type == "pand-incl" || type == "pand<=") {
112 builder.addPandGate(name, childNames, true);
113 } else if (type == "pand-excl" || type == "pand<") {
114 builder.addPandGate(name, childNames, false);
115 } else if (type == "por") {
116 builder.addPorGate(name, childNames);
117 } else if (type == "por-incl" || type == "por<=") {
118 builder.addPorGate(name, childNames, true);
119 } else if (type == "por-excl" || type == "por<") {
120 builder.addPorGate(name, childNames, false);
121 } else if (type == "wsp" || type == "csp" || type == "hsp" || type == "spare") {
122 builder.addSpareGate(name, childNames);
123 } else if (type == "seq") {
124 builder.addSequenceEnforcer(name, childNames);
125 } else if (type == "mutex") {
126 builder.addMutex(name, childNames);
127 } else if (type == "fdep") {
128 builder.addPdep(name, childNames, storm::utility::one<ValueType>());
129 } else if (boost::starts_with(type, "pdep=")) {
130 ValueType probability = valueParser.parseValue(type.substr(5));
131 builder.addPdep(name, childNames, probability);
132 } else if (type.find("=") != std::string::npos) {
133 // Use dedicated method for parsing BEs
134 // Remove name from line and parse remainder
135 std::regex regexName("\"?" + tokens[0] + "\"?");
136 std::string remaining_line = std::regex_replace(line, regexName, "");
137 parseBasicElement(name, remaining_line, builder, valueParser);
138 } else if (type.find("insp") != std::string::npos) {
139 // Inspection as defined by DFTCalc
140 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Inspections are not supported.");
141 } else {
142 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name '" << type << "' not recognized.");
143 }
144 }
145 }
146 } catch (storm::exceptions::BaseException const& exception) {
147 STORM_LOG_THROW(false, storm::exceptions::FileIoException, "A parsing exception occurred in line " << lineNo << ": " << exception.what());
148 }
149 builder.setTopLevel(toplevelId);
151
152 // Build DFT
154 STORM_LOG_DEBUG("DFT elements:\n" << dft.getElementsString());
155 STORM_LOG_DEBUG("Spare modules:\n" << dft.getModulesString());
156 return dft;
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 << "'.");
230 phases = storm::parser::parseNumber<size_t>(value);
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 if (!value.empty()) {
294 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Repairs are not supported and will be ignored for basic element '" << name << "'.");
295 }
296
297 boost::trim(input);
298 if (input != "") {
299 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Unknown arguments for basic element '" << name << "': " << input);
300 }
301
302 // Create BE with given distribution
303 STORM_LOG_THROW(distribution.has_value(), storm::exceptions::WrongFormatException, "No failure distribution is defined for BE '" << name << "'.");
304 switch (distribution.value()) {
305 case BEType::PROBABILITY:
306 STORM_LOG_THROW(prob.has_value(), storm::exceptions::WrongFormatException,
307 "Distribution " << toString(BEType::PROBABILITY) << " requires parameter 'prob' for BE '" << name << "'.");
308 if (!dorm.has_value()) {
309 STORM_LOG_WARN("No dormancy factor was provided for basic element '" << name << "'. Assuming dormancy factor of 1.");
310 dorm = storm::utility::one<ValueType>();
311 }
312 builder.addBasicElementProbability(name, prob.value(), dorm.value());
313 break;
314 case BEType::EXPONENTIAL:
315 STORM_LOG_THROW(lambda.has_value(), storm::exceptions::WrongFormatException,
316 "Distribution " << toString(BEType::EXPONENTIAL) << " requires parameter 'lambda' for BE '" << name << "'.");
317 if (!dorm.has_value()) {
318 STORM_LOG_WARN("No dormancy factor was provided for basic element '" << name << "'. Assuming dormancy factor of 1.");
319 dorm = storm::utility::one<ValueType>();
320 }
321 builder.addBasicElementExponential(name, lambda.value(), dorm.value());
322 break;
323 case BEType::ERLANG:
324 STORM_LOG_THROW(lambda.has_value(), storm::exceptions::WrongFormatException,
325 "Distribution " << toString(BEType::ERLANG) << " requires parameter 'lambda' for BE '" << name << "'.");
326 STORM_LOG_THROW(phases.has_value(), storm::exceptions::WrongFormatException,
327 "Distribution " << toString(BEType::ERLANG) << " requires parameter 'phases' for BE '" << name << "'.");
328 if (!dorm.has_value()) {
329 STORM_LOG_WARN("No dormancy factor was provided for basic element '" << name << "'. Assuming dormancy factor of 1.");
330 dorm = storm::utility::one<ValueType>();
331 }
332 builder.addBasicElementErlang(name, lambda.value(), phases.value(), dorm.value());
333 break;
334 case BEType::WEIBULL:
335 STORM_LOG_THROW(shape.has_value(), storm::exceptions::WrongFormatException,
336 "Distribution " << toString(BEType::WEIBULL) << " requires parameter 'shape' for BE '" << name << "'.");
337 STORM_LOG_THROW(rate.has_value(), storm::exceptions::WrongFormatException,
338 "Distribution " << toString(BEType::WEIBULL) << " requires parameter 'rate' for BE '" << name << "'.");
339 builder.addBasicElementWeibull(name, shape.value(), rate.value());
340 break;
341 case BEType::LOGNORMAL:
342 STORM_LOG_THROW(mean.has_value(), storm::exceptions::WrongFormatException,
343 "Distribution " << toString(BEType::LOGNORMAL) << " requires parameter 'mean' for BE '" << name << "'.");
344 STORM_LOG_THROW(stddev.has_value(), storm::exceptions::WrongFormatException,
345 "Distribution " << toString(BEType::WEIBULL) << " requires parameter 'stddev' for BE '" << name << "'.");
346 builder.addBasicElementLogNormal(name, mean.value(), stddev.value());
347 break;
348 default:
349 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "No distribution defined for basic element '" << name << "'.");
350 break;
351 }
352}
353
354// Explicitly instantiate the class.
355template class DFTGalileoParser<double>;
356template class DFTGalileoParser<RationalFunction>;
357
358} // namespace parser
359} // namespace storm::dft
void addPdep(std::string const &name, std::vector< std::string > const &children, ValueType probability)
Create (probabilistic) dependency (PDEP) and add it to DFT.
void addOrGate(std::string const &name, std::vector< std::string > const &children)
Create OR-gate and add it to DFT.
void addVotingGate(std::string const &name, unsigned threshold, std::vector< std::string > const &children)
Create VOTing-gate and add it to DFT.
void addBasicElementErlang(std::string const &name, ValueType rate, unsigned phases, ValueType dormancyFactor)
Create BE with Erlang distribution and add it to DFT.
void addSpareGate(std::string const &name, std::vector< std::string > const &children)
Create SPARE-gate and add it to DFT.
storm::dft::storage::DFT< ValueType > build()
Create DFT.
void addAndGate(std::string const &name, std::vector< std::string > const &children)
Create AND-gate 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 setTopLevel(std::string const &tle)
Set top level element.
void addBasicElementExponential(std::string const &name, ValueType rate, ValueType dormancyFactor, bool transient=false)
Create BE with exponential distribution and add it to DFT.
void addPorGate(std::string const &name, std::vector< std::string > const &children, bool inclusive=true)
Create POR-gate and add it to DFT.
void addSequenceEnforcer(std::string const &name, std::vector< std::string > const &children)
Create sequence enforcer (SEQ) and add it to DFT.
void addPandGate(std::string const &name, std::vector< std::string > const &children, bool inclusive=true)
Create PAND-gate 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.
void addMutex(std::string const &name, std::vector< std::string > const &children)
Create mutual exclusion-gate (MUTEX) 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.
Represents a Dynamic Fault Tree.
Definition DFT.h:52
std::string getModulesString() const
Definition DFT.cpp:527
std::string getElementsString() const
Definition DFT.cpp:511
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:30
#define STORM_LOG_DEBUG(message)
Definition logging.h:23
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
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