Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DFTJsonParser.cpp
Go to the documentation of this file.
1#include "DFTJsonParser.h"
2
3#include <boost/algorithm/string.hpp>
4#include <iostream>
5
12#include "storm/io/file.h"
14
15namespace storm::dft {
16namespace parser {
17
18template<typename ValueType>
20 std::ifstream file;
21 storm::io::openFile(filename, file);
22 Json jsonInput;
23 file >> jsonInput;
25 return parseJson(jsonInput);
26}
27
28template<typename ValueType>
30 Json jsonInput = Json::parse(jsonString);
31 return parseJson(jsonInput);
32}
33
34template<typename ValueType>
36 // Initialize DFT builder and value parser
39 std::string toplevelName = "";
41
42 std::string currentLocation;
43 try {
44 // Try to parse parameters
45 currentLocation = "parameters";
46 if (jsonInput.count("parameters") > 0) {
47 Json parameters = jsonInput.at("parameters");
48 STORM_LOG_THROW(parameters.empty() || (std::is_same<ValueType, storm::RationalFunction>::value), storm::exceptions::NotSupportedException,
49 "Parameters are only allowed when using rational functions.");
50 for (auto const& parameter : parameters) {
51 valueParser.addParameter(parseValue(parameter));
52 }
53 }
54
55 currentLocation = "nodes";
56 Json const& nodes = jsonInput.at("nodes");
57 // Start by building mapping from ids to their unique names
58 std::map<std::string, std::string> nameMapping;
59 std::set<std::string> names;
60 for (auto const& element : nodes) {
61 Json data = element.at("data");
62 std::string id = data.at("id");
63 std::string name = parseName(data.at("name"));
64 STORM_LOG_THROW(names.find(name) == names.end(), storm::exceptions::WrongFormatException, "Element '" << name << "' was already declared.");
65 names.insert(name);
66 nameMapping[id] = name;
67 }
68
69 // Parse nodes
70 for (auto const& element : nodes) {
71 currentLocation = parseValue(element);
72 Json const& data = element.at("data");
73 std::string name = parseName(data.at("name"));
74 // TODO: use contains() if modernjson is updated
75 if (data.count("relevant") > 0) {
76 bool isRelevant = data.at("relevant");
77 if (isRelevant) {
78 relevantEvents.insert(name);
79 }
80 }
81 // Create list of children
82 std::vector<std::string> childNames;
83 // TODO: use contains() if modernjson is updated
84 if (data.count("children") > 0) {
85 for (auto const& child : data.at("children")) {
86 STORM_LOG_THROW(nameMapping.find(child) != nameMapping.end(), storm::exceptions::WrongFormatException,
87 "Child '" << child << "' for element '" << name << "' was not defined.");
88 childNames.push_back(nameMapping.at(child));
89 }
90 }
91
92 std::string type = data.at("type");
93 if (type == "and") {
94 builder.addAndGate(name, childNames);
95 } else if (type == "or") {
96 builder.addOrGate(name, childNames);
97 } else if (type == "vot") {
98 STORM_LOG_THROW(data.count("voting") > 0, storm::exceptions::WrongFormatException, "Voting gate '" << name << "' requires parameter 'voting'.");
99 std::string votThreshold = parseValue(data.at("voting"));
100 builder.addVotingGate(name, storm::parser::parseNumber<size_t>(votThreshold), childNames);
101 } else if (type == "pand") {
102 if (data.count("inclusive") > 0) {
103 bool inclusive = data.at("inclusive");
104 builder.addPandGate(name, childNames, inclusive);
105 } else {
106 builder.addPandGate(name, childNames);
107 }
108 } else if (type == "por") {
109 if (data.count("inclusive") > 0) {
110 bool inclusive = data.at("inclusive");
111 builder.addPorGate(name, childNames, inclusive);
112 } else {
113 builder.addPorGate(name, childNames);
114 }
115 } else if (type == "spare") {
116 builder.addSpareGate(name, childNames);
117 } else if (type == "seq") {
118 builder.addSequenceEnforcer(name, childNames);
119 } else if (type == "mutex") {
120 builder.addMutex(name, childNames);
121 } else if (type == "fdep") {
122 builder.addPdep(name, childNames, storm::utility::one<ValueType>());
123 } else if (type == "pdep") {
124 STORM_LOG_THROW(data.count("probability") > 0, storm::exceptions::WrongFormatException,
125 "PDEP '" << name << "' requires parameter 'probability'.");
126 ValueType probability = valueParser.parseValue(parseValue(data.at("probability")));
127 if (storm::utility::isZero<ValueType>(probability)) {
128 // Skip element. Otherwise, trying to add layout information later on will fail
129 STORM_LOG_WARN("Dependency " << name << " with probability 0 is superfluous and will not be added.");
130 continue;
131 }
132 builder.addPdep(name, childNames, probability);
133 } else if (boost::starts_with(type, "be")) {
134 parseBasicElement(name, type, data, builder, valueParser);
135 } else if (type == "compound") {
136 STORM_LOG_TRACE("Ignoring compound node '" << name << "'.");
137 } else {
138 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name '" << type << "' not recognized.");
139 }
140
141 if (element.find("position") != element.end()) {
142 // Set layout positions
143 Json position = element.at("position");
144 double x = position.at("x");
145 double y = position.at("y");
146 builder.addLayoutInfo(name, x / 7, y / 7);
147 }
148 }
149
150 STORM_LOG_THROW(jsonInput.count("toplevel") > 0, storm::exceptions::WrongFormatException,
151 "Top level element must be specified via parameter 'toplevel'.");
152 std::string topLevelId = parseValue(jsonInput.at("toplevel"));
153 STORM_LOG_THROW(nameMapping.find(topLevelId) != nameMapping.end(), storm::exceptions::WrongFormatException,
154 "Top level element with id '" << topLevelId << "' was not defined.");
155 builder.setTopLevel(nameMapping.at(topLevelId));
156
157 } catch (storm::exceptions::BaseException const& exception) {
158 STORM_LOG_THROW(false, storm::exceptions::FileIoException, "A parsing exception occurred in " << currentLocation << ": " << exception.what());
159 } catch (std::exception const& exception) {
160 STORM_LOG_THROW(false, storm::exceptions::FileIoException, "An exception occurred during parsing in " << currentLocation << ": " << exception.what());
161 }
162
163 // Build DFT
165 // Set relevant events
166 dft.setRelevantEvents(relevantEvents, false);
167 STORM_LOG_DEBUG("Relevant events: " << dft.getRelevantEventsString());
168 return dft;
169}
170
171template<typename ValueType>
172std::string DFTJsonParser<ValueType>::parseName(std::string const& name) {
173 std::string newName = name;
174 std::replace(newName.begin(), newName.end(), ' ', '_');
175 std::replace(newName.begin(), newName.end(), '-', '_');
176 return newName;
177}
178
179template<typename ValueType>
180std::string DFTJsonParser<ValueType>::parseValue(Json value) {
181 if (value.is_string()) {
182 return value.get<std::string>();
183 } else {
184 std::stringstream stream;
185 stream << value;
186 return stream.str();
187 }
188}
189
190template<typename ValueType>
191void DFTJsonParser<ValueType>::parseBasicElement(std::string const& name, std::string const& type, Json input,
193 std::string distribution = "exponential"; // Default is exponential distribution
194 if (input.count("distribution") > 0) {
195 distribution = input.at("distribution");
196 // Handle short-form for exponential distribution
197 if (distribution == "exp") {
198 distribution = "exponential";
199 }
200 }
201 STORM_LOG_THROW(type == "be" || (type == "be_exp" && distribution == "exponential"), storm::exceptions::WrongFormatException,
202 "BE type '" << type << "' and distribution '" << distribution << " do not agree.");
203
204 if (distribution == "const") {
205 // Constant failed/failsafe
206 STORM_LOG_THROW(input.count("failed") > 0, storm::exceptions::WrongFormatException, "Constant BE '" << name << "' requires parameter 'failed'.");
207 bool failed = input.at("failed");
208 builder.addBasicElementConst(name, failed);
209 } else if (distribution == "probability") {
210 // Constant probability distribution
211 STORM_LOG_THROW(input.count("prob") > 0, storm::exceptions::WrongFormatException,
212 "BE '" << name << "' with probability distribution requires parameter 'prob'.");
213 ValueType probability = valueParser.parseValue(parseValue(input.at("prob")));
214 ValueType dormancy = storm::utility::one<ValueType>();
215 if (input.count("dorm") > 0) {
216 dormancy = valueParser.parseValue(parseValue(input.at("dorm")));
217 } else {
218 STORM_LOG_WARN("No dormancy factor was provided for basic element '" << name << "'. Assuming dormancy factor of 1.");
219 }
220 builder.addBasicElementProbability(name, probability, dormancy);
221 } else if (distribution == "exponential") {
222 // Exponential distribution
223 STORM_LOG_THROW(input.count("rate") > 0, storm::exceptions::WrongFormatException,
224 "BE '" << name << "' with exponential distribution requires parameter 'rate'.");
225 ValueType rate = valueParser.parseValue(parseValue(input.at("rate")));
226 ValueType dormancy = storm::utility::one<ValueType>();
227 if (input.count("dorm") > 0) {
228 dormancy = valueParser.parseValue(parseValue(input.at("dorm")));
229 } else {
230 STORM_LOG_WARN("No dormancy factor was provided for basic element '" << name << "'. Assuming dormancy factor of 1.");
231 }
232 bool transient = false;
233 if (input.count("transient") > 0) {
234 transient = input.at("transient");
235 }
236 builder.addBasicElementExponential(name, rate, dormancy, transient);
237 } else if (distribution == "erlang") {
238 // Erlang distribution
239 STORM_LOG_THROW(input.count("rate") > 0, storm::exceptions::WrongFormatException,
240 "BE '" << name << "' with Erlang distribution requires parameter 'rate'.");
241 ValueType rate = valueParser.parseValue(parseValue(input.at("rate")));
242 STORM_LOG_THROW(input.count("phases") > 0, storm::exceptions::WrongFormatException,
243 "BE '" << name << "' with Erlang distribution requires parameter 'phases'.");
244 size_t phases = storm::parser::parseNumber<size_t>(parseValue(input.at("phases")));
245 ValueType dormancy = storm::utility::one<ValueType>();
246 if (input.count("dorm") > 0) {
247 dormancy = valueParser.parseValue(parseValue(input.at("dorm")));
248 } else {
249 STORM_LOG_WARN("No dormancy factor was provided for basic element '" << name << "'. Assuming dormancy factor of 1.");
250 }
251 builder.addBasicElementErlang(name, rate, phases, dormancy);
252 } else if (distribution == "weibull") {
253 // Weibull distribution
254 STORM_LOG_THROW(input.count("shape") > 0, storm::exceptions::WrongFormatException,
255 "BE '" << name << "' with Weibull distribution requires parameter 'shape'.");
256 ValueType shape = valueParser.parseValue(parseValue(input.at("shape")));
257 STORM_LOG_THROW(input.count("rate") > 0, storm::exceptions::WrongFormatException,
258 "BE '" << name << "' with Weibull distribution requires parameter 'rate'.");
259 ValueType rate = valueParser.parseValue(parseValue(input.at("rate")));
260 builder.addBasicElementWeibull(name, shape, rate);
261 } else if (distribution == "lognormal") {
262 // Log-normal distribution
263 STORM_LOG_THROW(input.count("mean") > 0, storm::exceptions::WrongFormatException,
264 "BE '" << name << "' with Log-normal distribution requires parameter 'mean'.");
265 ValueType mean = valueParser.parseValue(parseValue(input.at("mean")));
266 STORM_LOG_THROW(input.count("stddev") > 0, storm::exceptions::WrongFormatException,
267 "BE '" << name << "' with Log-normal distribution requires parameter 'stddev'.");
268 ValueType stddev = valueParser.parseValue(parseValue(input.at("stddev")));
269 builder.addBasicElementLogNormal(name, mean, stddev);
270 } else {
271 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Distribution " << distribution << " not known.");
272 }
273}
274
275// Explicitly instantiate the class.
276template class DFTJsonParser<double>;
277template class DFTJsonParser<RationalFunction>;
278
279} // namespace parser
280} // 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 addLayoutInfo(std::string const &name, double x, double y)
Add layout information for DFT element.
void addSpareGate(std::string const &name, std::vector< std::string > const &children)
Create SPARE-gate and add it to DFT.
void addBasicElementConst(std::string const &name, bool failed)
Create BE which is constant failed or constant failsafe 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 custom JSON format.
static storm::dft::storage::DFT< ValueType > parseJsonFromFile(std::string const &filename)
Parse DFT from JSON format given as file and build DFT.
static storm::dft::storage::DFT< ValueType > parseJsonFromString(std::string const &jsonString)
Parse DFT from JSON format given as a string and build DFT.
Represents a Dynamic Fault Tree.
Definition DFT.h:52
std::string getRelevantEventsString() const
Get a string containing the list of all relevant events.
Definition DFT.cpp:716
void setRelevantEvents(storm::dft::utility::RelevantEvents const &relevantEvents, bool const allowDCForRelevant) const
Set the relevance flag for all elements according to the given relevant events.
Definition DFT.cpp:690
void insert(std::string const &name)
Add relevant event.
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_TRACE(message)
Definition logging.h:17
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SFTBDDChecker::ValueType ValueType
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