Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DFTBuilder.cpp
Go to the documentation of this file.
1#include "DFTBuilder.h"
2
3#include <algorithm>
4
9
12
13namespace storm::dft {
14namespace builder {
15
16template<typename ValueType>
17DFTBuilder<ValueType>::DFTBuilder() : mNextId(0), comparator() {
18 // Intentionally left empty
19}
20
21template<>
22DFTBuilder<double>::DFTBuilder() : mNextId(0), comparator(0 /* Set error to 0*/) {
23 // Intentionally left empty
24}
25
26template<typename ValueType>
28 STORM_LOG_THROW(!mTopLevelName.empty(), storm::exceptions::WrongFormatException, "No top level element defined.");
29
30 // Build parent/child connections for gates
31 for (auto& gateChildrenPair : mChildNames) {
32 STORM_LOG_ASSERT(gateChildrenPair.first->isGate(), "Element " << *gateChildrenPair.first << " with children is not a gate.");
33 DFTGatePointer gate = std::static_pointer_cast<storm::dft::storage::elements::DFTGate<ValueType>>(gateChildrenPair.first);
34 for (std::string const& childName : gateChildrenPair.second) {
35 auto itFind = mElements.find(childName);
36 STORM_LOG_THROW(itFind != mElements.end(), storm::exceptions::WrongFormatException,
37 "Child '" << childName << "' for gate '" << gate->name() << "' not found.");
38 DFTElementPointer childElement = itFind->second;
39 if (childElement->isRestriction()) {
40 STORM_LOG_WARN("Restriction '" << childName << "' is ignored as input for gate '" << gate->name() << "', because restrictions have no output.");
41 } else if (childElement->isDependency()) {
42 STORM_LOG_WARN("Dependency '" << childName << "' is ignored as input for gate '" << gate->name() << "', because dependencies have no output.");
43 } else {
44 gate->addChild(childElement);
45 childElement->addParent(gate);
46 }
47 }
48 }
49
50 // Build connections for restrictions
51 for (auto& restrictionChildrenPair : mRestrictionChildNames) {
52 DFTRestrictionPointer restriction = restrictionChildrenPair.first;
53 for (std::string const& childName : restrictionChildrenPair.second) {
54 auto itFind = mElements.find(childName);
55 STORM_LOG_THROW(itFind != mElements.end(), storm::exceptions::WrongFormatException,
56 "Child '" << childName << "' for restriction '" << restriction->name() << "' not found.");
57 DFTElementPointer childElement = itFind->second;
58 STORM_LOG_THROW(childElement->isGate() || childElement->isBasicElement(), storm::exceptions::WrongFormatException,
59 "Child '" << childElement->name() << "' of restriction '" << restriction->name() << "' must be gate or BE.");
60 restriction->addChild(childElement);
61 childElement->addRestriction(restriction);
62 }
63 }
64
65 // Build connections for dependencies
66 for (auto& dependencyChildrenPair : mDependencyChildNames) {
67 DFTDependencyPointer dependency = dependencyChildrenPair.first;
68 bool triggerElement = true;
69 for (std::string const& childName : dependencyChildrenPair.second) {
70 auto itFind = mElements.find(childName);
71 STORM_LOG_THROW(itFind != mElements.end(), storm::exceptions::WrongFormatException,
72 "Child '" << childName << "' for dependency '" << dependency->name() << "' not found.");
73 DFTElementPointer childElement = itFind->second;
74 if (triggerElement) {
75 triggerElement = false;
76 STORM_LOG_THROW(childElement->isGate() || childElement->isBasicElement(), storm::exceptions::WrongFormatException,
77 "Trigger element '" << childName << "' of dependency '" << dependency->name() << "' must be gate or BE.");
78 dependency->setTriggerElement(std::static_pointer_cast<storm::dft::storage::elements::DFTGate<ValueType>>(childElement));
79 childElement->addOutgoingDependency(dependency);
80 } else {
81 STORM_LOG_THROW(childElement->isBasicElement(), storm::exceptions::WrongFormatException,
82 "Dependent element '" << childName << "' of dependency '" << dependency->name() << "' must be BE.");
83 DFTBEPointer dependentBE = std::static_pointer_cast<storm::dft::storage::elements::DFTBE<ValueType>>(childElement);
84 dependency->addDependentEvent(dependentBE);
85 dependentBE->addIngoingDependency(dependency);
86 }
87 }
88 }
89
90 // Sort elements topologically
91 DFTElementVector elements = sortTopological();
92 // Set ids according to order
93 size_t id = 0;
94 for (DFTElementPointer e : elements) {
95 e->setId(id++);
96 }
97 // Compute rank
98 computeRank(mElements[mTopLevelName]); // Start with top level element
99 for (auto& elem : mElements) {
100 computeRank(elem.second);
101 }
102
103 // Create DFT
104 storm::dft::storage::DFT<ValueType> dft(elements, mElements[mTopLevelName]);
105
106 // Set default BE order from topological order
107 std::vector<size_t> beOrder;
108 for (auto elem : mElements) {
109 if (elem.second->isBasicElement()) {
110 beOrder.push_back(elem.second->id());
111 }
112 }
113 std::sort(beOrder.begin(), beOrder.end());
114 dft.setBEOrder(beOrder);
115
116 // Set layout info
117 for (auto& elem : mElements) {
118 if (mLayoutInfo.count(elem.first) > 0) {
119 // Use given layout info
120 dft.setElementLayoutInfo(elem.second->id(), mLayoutInfo.at(elem.first));
121 } else {
122 // Set default layout
124 }
125 }
126
127 return dft;
128}
129
130template<typename ValueType>
131void DFTBuilder<ValueType>::addElement(DFTElementPointer element) {
132 STORM_LOG_THROW(!nameInUse(element->name()), storm::exceptions::InvalidArgumentException, "Element with name '" << element->name() << "' already exists.");
133 STORM_LOG_ASSERT(mNextId == mElements.size(), "Current id " << mNextId << " and number of elements " << mElements.size() << " do not match.");
134 element->setId(mNextId++);
135 mElements[element->name()] = element;
136}
137
138template<typename ValueType>
139void DFTBuilder<ValueType>::addBasicElementConst(std::string const& name, bool failed) {
140 addElement(std::make_shared<storm::dft::storage::elements::BEConst<ValueType>>(0, name, failed));
141}
142
143template<typename ValueType>
144void DFTBuilder<ValueType>::addBasicElementProbability(std::string const& name, ValueType probability, ValueType dormancyFactor) {
145 // Handle special cases
146 if (storm::utility::isZero<ValueType>(probability)) {
147 addBasicElementConst(name, false);
148 } else if (storm::utility::isOne<ValueType>(probability)) {
149 addBasicElementConst(name, true);
150 } else {
151 STORM_LOG_THROW(isValidProbability(probability), storm::exceptions::WrongFormatException,
152 "Failure probability " << probability << " of BE " << name << " is not within interval [0, 1].");
153 STORM_LOG_THROW(isValidProbability(dormancyFactor), storm::exceptions::WrongFormatException,
154 "Dormancy factor " << dormancyFactor << " of BE " << name << " is not within interval [0, 1].");
155 addElement(std::make_shared<storm::dft::storage::elements::BEProbability<ValueType>>(0, name, probability, dormancyFactor));
156 }
157}
158
159template<typename ValueType>
160void DFTBuilder<ValueType>::addBasicElementExponential(std::string const& name, ValueType rate, ValueType dormancyFactor, bool transient) {
161 // Handle special cases
162 if (storm::utility::isZero<ValueType>(rate)) {
163 addBasicElementConst(name, false);
164 } else {
165 STORM_LOG_THROW(this->comparator.isLess(storm::utility::zero<ValueType>(), rate), storm::exceptions::WrongFormatException,
166 "Failure rate " << rate << " of BE " << name << " must be positive.");
167 STORM_LOG_THROW(isValidProbability(dormancyFactor), storm::exceptions::WrongFormatException,
168 "Dormancy factor " << dormancyFactor << " of BE " << name << " is not within interval [0, 1].");
169 addElement(std::make_shared<storm::dft::storage::elements::BEExponential<ValueType>>(0, name, rate, dormancyFactor, transient));
170 }
171}
172
173template<typename ValueType>
174void DFTBuilder<ValueType>::addBasicElementErlang(std::string const& name, ValueType rate, unsigned phases, ValueType dormancyFactor) {
175 // Handle special cases
176 if (storm::utility::isZero<ValueType>(rate)) {
177 addBasicElementConst(name, false);
178 } else if (phases == 1) {
179 // shape=1 reduces to exponential distribution
180 addBasicElementExponential(name, rate, dormancyFactor);
181 } else {
182 STORM_LOG_THROW(this->comparator.isLess(storm::utility::zero<ValueType>(), rate), storm::exceptions::WrongFormatException,
183 "Erlang distribution of BE " << name << " requires a positive rate.");
184 STORM_LOG_THROW(phases > 0, storm::exceptions::WrongFormatException, "Erlang distribution of BE " << name << " requires a positive number of phases.");
185 STORM_LOG_THROW(isValidProbability(dormancyFactor), storm::exceptions::WrongFormatException,
186 "Dormancy factor " << dormancyFactor << " of BE " << name << " is not within interval [0, 1].");
187 addElement(std::make_shared<storm::dft::storage::elements::BEErlang<ValueType>>(0, name, rate, phases, dormancyFactor));
188 }
189}
190
191template<typename ValueType>
192void DFTBuilder<ValueType>::addBasicElementWeibull(std::string const& name, ValueType shape, ValueType rate) {
193 STORM_LOG_THROW(this->comparator.isLess(storm::utility::zero<ValueType>(), rate), storm::exceptions::WrongFormatException,
194 "Weibull distribution of BE " << name << " requires a positive scale.");
195 STORM_LOG_THROW(this->comparator.isLess(storm::utility::zero<ValueType>(), shape), storm::exceptions::WrongFormatException,
196 "Weibull distribution of BE " << name << " requires a positive shape.");
197
198 // Handle special cases
199 if (storm::utility::isOne<ValueType>(shape)) {
200 // shape=1 reduces to exponential distribution with rate 1/lambda
201 addBasicElementExponential(name, storm::utility::one<ValueType>() / rate, storm::utility::one<ValueType>());
202 } else {
203 addElement(std::make_shared<storm::dft::storage::elements::BEWeibull<ValueType>>(0, name, shape, rate));
204 }
205}
206
207template<typename ValueType>
208void DFTBuilder<ValueType>::addBasicElementLogNormal(std::string const& name, ValueType mean, ValueType standardDeviation) {
209 STORM_LOG_THROW(this->comparator.isLess(storm::utility::zero<ValueType>(), standardDeviation), storm::exceptions::WrongFormatException,
210 "Log-normal distribution of BE " << name << " requires a positive standard deviation.");
211 addElement(std::make_shared<storm::dft::storage::elements::BELogNormal<ValueType>>(0, name, mean, standardDeviation));
212}
213
214template<typename ValueType>
215void DFTBuilder<ValueType>::addBasicElementSamples(std::string const& name, std::map<ValueType, ValueType> const& activeSamples) {
216 // Check if it can fail
217 bool canFail = false;
218 for (auto const& sample : activeSamples) {
219 // At least one sample is not zero
220 if (!storm::utility::isZero(sample.second)) {
221 canFail = true;
222 break;
223 }
224 }
225 if (!canFail) {
226 // Add constant failed BE instead
227 addBasicElementConst(name, false);
228 } else {
229 addElement(std::make_shared<storm::dft::storage::elements::BESamples<ValueType>>(0, name, activeSamples));
230 }
231}
232
233template<typename ValueType>
234void DFTBuilder<ValueType>::addGate(DFTGatePointer gate, std::vector<std::string> const& children) {
235 STORM_LOG_THROW(children.size() > 0, storm::exceptions::WrongFormatException, "No children given for gate " << gate << ".");
236 mChildNames[gate] = children;
237 addElement(gate);
238}
239
240template<typename ValueType>
241void DFTBuilder<ValueType>::addAndGate(std::string const& name, std::vector<std::string> const& children) {
242 addGate(std::make_shared<storm::dft::storage::elements::DFTAnd<ValueType>>(0, name), children);
243}
244
245template<typename ValueType>
246void DFTBuilder<ValueType>::addOrGate(std::string const& name, std::vector<std::string> const& children) {
247 addGate(std::make_shared<storm::dft::storage::elements::DFTOr<ValueType>>(0, name), children);
248}
249
250template<typename ValueType>
251void DFTBuilder<ValueType>::addVotingGate(std::string const& name, unsigned threshold, std::vector<std::string> const& children) {
252 STORM_LOG_THROW(threshold <= children.size(), storm::exceptions::WrongFormatException,
253 "Voting gate " << name << " has threshold " << threshold << " higher than the number of children " << children.size() << ".");
254 // Handle special cases
255 if (children.size() == threshold) {
256 addAndGate(name, children);
257 } else if (threshold == 1) {
258 addOrGate(name, children);
259 } else {
260 addGate(std::make_shared<storm::dft::storage::elements::DFTVot<ValueType>>(0, name, threshold), children);
261 }
262}
263
264template<typename ValueType>
265void DFTBuilder<ValueType>::addPandGate(std::string const& name, std::vector<std::string> const& children, bool inclusive) {
266 addGate(std::make_shared<storm::dft::storage::elements::DFTPand<ValueType>>(0, name, inclusive), children);
267}
268
269template<typename ValueType>
270void DFTBuilder<ValueType>::addPorGate(std::string const& name, std::vector<std::string> const& children, bool inclusive) {
271 addGate(std::make_shared<storm::dft::storage::elements::DFTPor<ValueType>>(0, name, inclusive), children);
272}
273
274template<typename ValueType>
275void DFTBuilder<ValueType>::addSpareGate(std::string const& name, std::vector<std::string> const& children) {
276 addGate(std::make_shared<storm::dft::storage::elements::DFTSpare<ValueType>>(0, name), children);
277}
278
279template<typename ValueType>
280void DFTBuilder<ValueType>::addDependency(DFTDependencyPointer dependency, std::vector<std::string> const& children) {
281 STORM_LOG_THROW(children.size() > 1, storm::exceptions::WrongFormatException, "Dependency " << dependency->name() << " requires at least two children.");
282 if (storm::utility::isZero(dependency->probability())) {
283 STORM_LOG_WARN("Dependency " << dependency->name() << " with probability 0 is superfluous and will not be added.");
284 } else {
285 STORM_LOG_THROW(isValidProbability(dependency->probability()), storm::exceptions::WrongFormatException,
286 "Probability " << dependency->probability() << " of PDEP " << *dependency << " is not within interval [0, 1].");
287 mDependencyChildNames[dependency] = children;
288 addElement(dependency);
289 }
290}
291
292template<typename ValueType>
293void DFTBuilder<ValueType>::addPdep(std::string const& name, std::vector<std::string> const& children, ValueType probability) {
294 addDependency(std::make_shared<storm::dft::storage::elements::DFTDependency<ValueType>>(0, name, probability), children);
295}
296
297template<typename ValueType>
298void DFTBuilder<ValueType>::addRestriction(DFTRestrictionPointer restriction, std::vector<std::string> const& children) {
299 STORM_LOG_THROW(children.size() > 1, storm::exceptions::WrongFormatException, "Restriction " << restriction->name() << " requires at least two children.");
300 mRestrictionChildNames[restriction] = children;
301 addElement(restriction);
302}
303
304template<typename ValueType>
305void DFTBuilder<ValueType>::addSequenceEnforcer(std::string const& name, std::vector<std::string> const& children) {
306 addRestriction(std::make_shared<storm::dft::storage::elements::DFTSeq<ValueType>>(0, name), children);
307}
308
309template<typename ValueType>
310void DFTBuilder<ValueType>::addMutex(std::string const& name, std::vector<std::string> const& children) {
311 addRestriction(std::make_shared<storm::dft::storage::elements::DFTMutex<ValueType>>(0, name), children);
312}
313
314template<typename ValueType>
315void DFTBuilder<ValueType>::setTopLevel(std::string const& tle) {
316 STORM_LOG_THROW(mTopLevelName.empty(), storm::exceptions::WrongFormatException, "Top level element was already set");
317 STORM_LOG_THROW(nameInUse(tle), storm::exceptions::InvalidArgumentException, "Element with name '" << tle << "' not known.");
318 mTopLevelName = tle;
319}
320
321template<typename ValueType>
322void DFTBuilder<ValueType>::addLayoutInfo(std::string const& name, double x, double y) {
323 STORM_LOG_THROW(nameInUse(name), storm::exceptions::InvalidArgumentException, "Element with name '" << name << "' not found.");
324 mLayoutInfo[name] = storm::dft::storage::DFTLayoutInfo(x, y);
325}
326
327template<typename ValueType>
328void DFTBuilder<ValueType>::cloneElement(DFTElementCPointer element) {
329 switch (element->type()) {
331 addElement(element->clone());
332 break;
341 auto elemWithChildren = std::static_pointer_cast<storm::dft::storage::elements::DFTChildren<ValueType> const>(element);
342 std::vector<std::string> children{};
343 for (DFTElementPointer const& elem : elemWithChildren->children()) {
344 children.push_back(elem->name());
345 }
346 cloneElementWithNewChildren(elemWithChildren, children);
347 break;
348 }
350 auto dependency = std::static_pointer_cast<storm::dft::storage::elements::DFTDependency<ValueType> const>(element);
351 std::vector<std::string> children = {dependency->triggerEvent()->name()};
352 for (auto const& depEv : dependency->dependentEvents()) {
353 children.push_back(depEv->name());
354 }
355 addDependency(std::static_pointer_cast<storm::dft::storage::elements::DFTDependency<ValueType>>(dependency->clone()), children);
356 break;
357 }
358 default:
359 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "DFT element type '" << element->type() << "' not known.");
360 break;
361 }
362}
363
364template<typename ValueType>
365void DFTBuilder<ValueType>::cloneElementWithNewChildren(DFTChildrenCPointer elemWithChildren, std::vector<std::string> const& children) {
366 switch (elemWithChildren->type()) {
373 addGate(std::static_pointer_cast<storm::dft::storage::elements::DFTGate<ValueType>>(elemWithChildren->clone()), children);
374 break;
377 addRestriction(std::static_pointer_cast<storm::dft::storage::elements::DFTRestriction<ValueType>>(elemWithChildren->clone()), children);
378 break;
379 default:
380 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "DFT element type '" << elemWithChildren->type() << "' not known.");
381 break;
382 }
383}
384
385template<typename ValueType>
386void DFTBuilder<ValueType>::topologicalVisit(DFTElementPointer const& element,
387 std::map<DFTElementPointer, topoSortColour, storm::dft::storage::OrderElementsById<ValueType>>& visited,
388 DFTElementVector& visitedElements) {
389 STORM_LOG_THROW(visited[element] != topoSortColour::GREY, storm::exceptions::WrongFormatException, "DFT is cyclic.");
390 if (visited[element] == topoSortColour::WHITE) {
391 // Mark as currently visiting
392 visited[element] = topoSortColour::GREY;
393 // Element was not visited before
394 if (element->isGate()) {
395 for (DFTElementPointer const& child : std::static_pointer_cast<storm::dft::storage::elements::DFTGate<ValueType>>(element)->children()) {
396 // Recursively visit all children
397 topologicalVisit(child, visited, visitedElements);
398 }
399 }
400 // TODO: restrictions and dependencies have no parents, so this can be done more efficiently.
401 else if (element->isRestriction()) {
402 for (DFTElementPointer const& child : std::static_pointer_cast<storm::dft::storage::elements::DFTRestriction<ValueType>>(element)->children()) {
403 // Recursively visit all children
404 topologicalVisit(child, visited, visitedElements);
405 }
406 } else if (element->isDependency()) {
407 for (DFTElementPointer const& child :
408 std::static_pointer_cast<storm::dft::storage::elements::DFTDependency<ValueType>>(element)->dependentEvents()) {
409 // Recursively visit all dependent children
410 topologicalVisit(child, visited, visitedElements);
411 }
412 // Visit trigger element
413 topologicalVisit(std::static_pointer_cast<storm::dft::storage::elements::DFTDependency<ValueType>>(element)->triggerEvent(), visited,
414 visitedElements);
415 } else {
416 STORM_LOG_ASSERT(element->isBasicElement(), "Unknown element type " << element->type() << " for " << *element);
417 }
418 // Mark as completely visited
419 visited[element] = topoSortColour::BLACK;
420 // Children have all been visited before -> add element to list
421 visitedElements.push_back(element);
422 }
423}
424
425template<typename ValueType>
426bool DFTBuilder<ValueType>::nameInUse(std::string const& name) const {
427 return mElements.find(name) != mElements.end();
428}
429
430template<typename ValueType>
431bool DFTBuilder<ValueType>::isValidProbability(ValueType value) const {
432 if (this->comparator.isZero(value) || this->comparator.isOne(value)) {
433 return true;
434 } else if (!this->comparator.isConstant(value)) {
435 // Do not check further if value is non-constant rational function
436 return true;
437 } else if (this->comparator.isLess(storm::utility::zero<ValueType>(), value) && this->comparator.isLess(value, storm::utility::one<ValueType>())) {
438 return true;
439 }
440 return false;
441}
442
443template<typename ValueType>
444std::vector<std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType>>> DFTBuilder<ValueType>::sortTopological() {
445 // Prepare map
446 std::map<DFTElementPointer, topoSortColour, storm::dft::storage::OrderElementsById<ValueType>> visited;
447 for (auto const& e : mElements) {
448 visited.insert(std::make_pair(e.second, topoSortColour::WHITE));
449 }
450
451 DFTElementVector visitedElements; // Return argument
452 // Start from top level element
453 topologicalVisit(mElements[mTopLevelName], visited, visitedElements);
454 for (auto const& e : visited) {
455 // Visit all elements to account for restrictions/dependencies/etc. not directly reachable from top level element
456 topologicalVisit(e.first, visited, visitedElements);
457 }
458 return visitedElements;
459}
460
461template<typename ValueType>
462size_t DFTBuilder<ValueType>::computeRank(DFTElementPointer const& elem) {
463 if (elem->rank() == static_cast<decltype(elem->rank())>(-1)) {
464 // Compute rank
465 if (elem->isBasicElement() || elem->isDependency() || elem->isRestriction()) {
466 // Rank is 0 for BEs/dependencies/restrictions
467 elem->setRank(0);
468 } else {
469 // Rank is maximal rank of children + 1
470 DFTGatePointer gate = std::static_pointer_cast<storm::dft::storage::elements::DFTGate<ValueType>>(elem);
471 size_t maxRank = 0;
472 for (DFTElementPointer const& child : gate->children()) {
473 maxRank = std::max(maxRank, computeRank(child));
474 }
475 elem->setRank(maxRank + 1);
476 }
477 }
478
479 return elem->rank();
480}
481
482// Explicitly instantiate the class.
483template class DFTBuilder<double>;
484template class DFTBuilder<RationalFunction>;
485
486} // namespace builder
487} // 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 addBasicElementSamples(std::string const &name, std::map< ValueType, ValueType > const &activeSamples)
Create BE with distribution given by sample points 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 cloneElement(DFTElementCPointer element)
Clone element and add it via the builder.
void setTopLevel(std::string const &tle)
Set top level element.
void cloneElementWithNewChildren(DFTChildrenCPointer elemWithChildren, std::vector< std::string > const &children)
Clone element, replace its children with the given children and add it via the builder.
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.
Represents a Dynamic Fault Tree.
Definition DFT.h:52
void setBEOrder(std::vector< size_t > const &bes)
Set order of BEs.
Definition DFT.h:240
void setElementLayoutInfo(size_t id, DFTLayoutInfo const &layoutInfo)
Definition DFT.h:340
BE which is either constant failed or constant failsafe.
Definition BEConst.h:14
BE with Erlang failure distribution.
Definition BEErlang.h:13
BE with exponential failure distribution.
BE with log-normal failure distribution.
Definition BELogNormal.h:13
BE with constant (Bernoulli) failure probability distribution.
BE where the failure distribution is defined by samples.
Definition BESamples.h:16
BE with Weibull failure distribution.
Definition BEWeibull.h:13
Dependency gate with probability p.
Abstract base class for gates.
Definition DFTGate.h:13
Mutex restriction (MUTEX).
Definition DFTMutex.h:15
Priority AND (PAND) gate.
Definition DFTPand.h:17
Priority OR (POR) gate.
Definition DFTPor.h:17
Abstract base class for restrictions.
Sequence enforcer (SEQ).
Definition DFTSeq.h:15
VOT gate with threshold k.
Definition DFTVot.h:14
#define STORM_LOG_WARN(message)
Definition logging.h:30
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SFTBDDChecker::ValueType ValueType
bool isZero(ValueType const &a)
Definition constants.cpp:41
LabParser.cpp.
Definition cli.cpp:18