16template<
typename ValueType>
26template<
typename ValueType>
28 STORM_LOG_THROW(!mTopLevelName.empty(), storm::exceptions::WrongFormatException,
"No top level element defined.");
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.");
44 gate->addChild(childElement);
45 childElement->addParent(gate);
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);
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;
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.");
79 childElement->addOutgoingDependency(dependency);
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);
91 DFTElementVector elements = sortTopological();
94 for (DFTElementPointer e : elements) {
98 computeRank(mElements[mTopLevelName]);
99 for (
auto& elem : mElements) {
100 computeRank(elem.second);
107 std::vector<size_t> beOrder;
108 for (
auto elem : mElements) {
109 if (elem.second->isBasicElement()) {
110 beOrder.push_back(elem.second->id());
113 std::sort(beOrder.begin(), beOrder.end());
117 for (
auto& elem : mElements) {
118 if (mLayoutInfo.count(elem.first) > 0) {
130template<
typename ValueType>
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;
138template<
typename ValueType>
143template<
typename ValueType>
146 if (storm::utility::isZero<ValueType>(probability)) {
147 addBasicElementConst(name,
false);
148 }
else if (storm::utility::isOne<ValueType>(probability)) {
149 addBasicElementConst(name,
true);
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].");
159template<
typename ValueType>
162 if (storm::utility::isZero<ValueType>(rate)) {
163 addBasicElementConst(name,
false);
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].");
173template<
typename ValueType>
176 if (storm::utility::isZero<ValueType>(rate)) {
177 addBasicElementConst(name,
false);
178 }
else if (phases == 1) {
180 addBasicElementExponential(name, rate, dormancyFactor);
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].");
191template<
typename ValueType>
194 "Weibull distribution of BE " << name <<
" requires a positive scale.");
196 "Weibull distribution of BE " << name <<
" requires a positive shape.");
199 if (storm::utility::isOne<ValueType>(shape)) {
201 addBasicElementExponential(name, storm::utility::one<ValueType>() / rate, storm::utility::one<ValueType>());
207template<
typename ValueType>
210 "Log-normal distribution of BE " << name <<
" requires a positive standard deviation.");
214template<
typename ValueType>
217 bool canFail =
false;
218 for (
auto const& sample : activeSamples) {
227 addBasicElementConst(name,
false);
233template<
typename ValueType>
235 STORM_LOG_THROW(children.size() > 0, storm::exceptions::WrongFormatException,
"No children given for gate " << gate <<
".");
236 mChildNames[gate] = children;
240template<
typename ValueType>
245template<
typename ValueType>
250template<
typename ValueType>
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() <<
".");
255 if (children.size() == threshold) {
256 addAndGate(name, children);
257 }
else if (threshold == 1) {
258 addOrGate(name, children);
264template<
typename ValueType>
269template<
typename ValueType>
274template<
typename ValueType>
279template<
typename ValueType>
281 STORM_LOG_THROW(children.size() > 1, storm::exceptions::WrongFormatException,
"Dependency " << dependency->name() <<
" requires at least two children.");
283 STORM_LOG_WARN(
"Dependency " << dependency->name() <<
" with probability 0 is superfluous and will not be added.");
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);
292template<
typename ValueType>
297template<
typename ValueType>
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);
304template<
typename ValueType>
309template<
typename ValueType>
314template<
typename ValueType>
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.");
321template<
typename ValueType>
323 STORM_LOG_THROW(nameInUse(name), storm::exceptions::InvalidArgumentException,
"Element with name '" << name <<
"' not found.");
327template<
typename ValueType>
329 switch (element->type()) {
331 addElement(element->clone());
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());
346 cloneElementWithNewChildren(elemWithChildren, children);
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());
359 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"DFT element type '" << element->type() <<
"' not known.");
364template<
typename ValueType>
366 switch (elemWithChildren->type()) {
380 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"DFT element type '" << elemWithChildren->type() <<
"' not known.");
385template<
typename ValueType>
388 DFTElementVector& visitedElements) {
389 STORM_LOG_THROW(visited[element] != topoSortColour::GREY, storm::exceptions::WrongFormatException,
"DFT is cyclic.");
390 if (visited[element] == topoSortColour::WHITE) {
392 visited[element] = topoSortColour::GREY;
394 if (element->isGate()) {
395 for (DFTElementPointer
const& child :
std::static_pointer_cast<
storm::dft::storage::elements::DFTGate<ValueType>>(element)->children()) {
397 topologicalVisit(child, visited, visitedElements);
401 else if (element->isRestriction()) {
402 for (DFTElementPointer
const& child :
std::static_pointer_cast<
storm::dft::storage::elements::DFTRestriction<ValueType>>(element)->children()) {
404 topologicalVisit(child, visited, visitedElements);
406 }
else if (element->isDependency()) {
407 for (DFTElementPointer
const& child :
408 std::static_pointer_cast<
storm::dft::storage::elements::DFTDependency<
ValueType>>(element)->dependentEvents()) {
410 topologicalVisit(child, visited, visitedElements);
416 STORM_LOG_ASSERT(element->isBasicElement(),
"Unknown element type " << element->type() <<
" for " << *element);
419 visited[element] = topoSortColour::BLACK;
421 visitedElements.push_back(element);
425template<
typename ValueType>
426bool DFTBuilder<ValueType>::nameInUse(std::string
const& name)
const {
427 return mElements.find(name) != mElements.end();
430template<
typename ValueType>
431bool DFTBuilder<ValueType>::isValidProbability(ValueType value)
const {
440template<
typename ValueType>
441std::vector<std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType>>> DFTBuilder<ValueType>::sortTopological() {
443 std::map<DFTElementPointer, topoSortColour, storm::dft::storage::OrderElementsById<ValueType>> visited;
444 for (
auto const& e : mElements) {
445 visited.insert(std::make_pair(e.second, topoSortColour::WHITE));
448 DFTElementVector visitedElements;
450 topologicalVisit(mElements[mTopLevelName], visited, visitedElements);
451 for (
auto const& e : visited) {
453 topologicalVisit(e.first, visited, visitedElements);
455 return visitedElements;
458template<
typename ValueType>
459size_t DFTBuilder<ValueType>::computeRank(DFTElementPointer
const& elem) {
460 if (elem->rank() ==
static_cast<decltype(elem-
>rank())>(-1)) {
462 if (elem->isBasicElement() || elem->isDependency() || elem->isRestriction()) {
467 DFTGatePointer gate = std::static_pointer_cast<storm::dft::storage::elements::DFTGate<ValueType>>(elem);
469 for (DFTElementPointer
const& child : gate->children()) {
470 maxRank = std::max(maxRank, computeRank(child));
472 elem->setRank(maxRank + 1);
480template class DFTBuilder<double>;
481template class DFTBuilder<RationalFunction>;
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.
void setBEOrder(std::vector< size_t > const &bes)
Set order of BEs.
void setElementLayoutInfo(size_t id, DFTLayoutInfo const &layoutInfo)
BE which is either constant failed or constant failsafe.
BE with Erlang failure distribution.
BE with exponential failure distribution.
BE with log-normal failure distribution.
BE with constant (Bernoulli) failure probability distribution.
BE where the failure distribution is defined by samples.
BE with Weibull failure distribution.
Dependency gate with probability p.
Abstract base class for gates.
Mutex restriction (MUTEX).
Priority AND (PAND) gate.
Abstract base class for restrictions.
VOT gate with threshold k.
#define STORM_LOG_WARN(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
SFTBDDChecker::ValueType ValueType
bool isPositive(ValueType const &a)
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.
bool isZero(ValueType const &a)