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