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