15template<
typename ValueType>
25template<
typename ValueType>
27 STORM_LOG_THROW(!mTopLevelName.empty(), storm::exceptions::WrongFormatException,
"No top level element defined.");
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.");
43 gate->addChild(childElement);
44 childElement->addParent(gate);
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);
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;
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.");
78 childElement->addOutgoingDependency(dependency);
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);
90 DFTElementVector elements = sortTopological();
93 for (DFTElementPointer e : elements) {
97 computeRank(mElements[mTopLevelName]);
98 for (
auto& elem : mElements) {
99 computeRank(elem.second);
106 std::vector<size_t> beOrder;
107 for (
auto elem : mElements) {
108 if (elem.second->isBasicElement()) {
109 beOrder.push_back(elem.second->id());
112 std::sort(beOrder.begin(), beOrder.end());
116 for (
auto& elem : mElements) {
117 if (mLayoutInfo.count(elem.first) > 0) {
129template<
typename ValueType>
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;
137template<
typename ValueType>
142template<
typename ValueType>
145 if (storm::utility::isZero<ValueType>(probability)) {
146 addBasicElementConst(name,
false);
147 }
else if (storm::utility::isOne<ValueType>(probability)) {
148 addBasicElementConst(name,
true);
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].");
158template<
typename ValueType>
161 if (storm::utility::isZero<ValueType>(rate)) {
162 addBasicElementConst(name,
false);
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].");
172template<
typename ValueType>
175 if (storm::utility::isZero<ValueType>(rate)) {
176 addBasicElementConst(name,
false);
177 }
else if (phases == 1) {
179 addBasicElementExponential(name, rate, dormancyFactor);
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].");
190template<
typename ValueType>
193 "Weibull distribution of BE " << name <<
" requires a positive scale.");
195 "Weibull distribution of BE " << name <<
" requires a positive shape.");
198 if (storm::utility::isOne<ValueType>(shape)) {
200 addBasicElementExponential(name, storm::utility::one<ValueType>() / rate, storm::utility::one<ValueType>());
206template<
typename ValueType>
209 "Log-normal distribution of BE " << name <<
" requires a positive standard deviation.");
213template<
typename ValueType>
216 bool canFail =
false;
217 for (
auto const& sample : activeSamples) {
226 addBasicElementConst(name,
false);
232template<
typename ValueType>
234 STORM_LOG_THROW(children.size() > 0, storm::exceptions::WrongFormatException,
"No children given for gate " << gate <<
".");
235 mChildNames[gate] = children;
239template<
typename ValueType>
244template<
typename ValueType>
249template<
typename ValueType>
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() <<
".");
254 if (children.size() == threshold) {
255 addAndGate(name, children);
256 }
else if (threshold == 1) {
257 addOrGate(name, children);
263template<
typename ValueType>
268template<
typename ValueType>
273template<
typename ValueType>
278template<
typename ValueType>
280 STORM_LOG_THROW(children.size() > 1, storm::exceptions::WrongFormatException,
"Dependency " << dependency->name() <<
" requires at least two children.");
282 STORM_LOG_WARN(
"Dependency " << dependency->name() <<
" with probability 0 is superfluous and will not be added.");
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);
291template<
typename ValueType>
296template<
typename ValueType>
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);
303template<
typename ValueType>
308template<
typename ValueType>
313template<
typename ValueType>
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.");
320template<
typename ValueType>
322 STORM_LOG_THROW(nameInUse(name), storm::exceptions::InvalidArgumentException,
"Element with name '" << name <<
"' not found.");
326template<
typename ValueType>
328 switch (element->type()) {
330 addElement(element->clone());
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());
345 cloneElementWithNewChildren(elemWithChildren, children);
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());
358 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"DFT element type '" << element->type() <<
"' not known.");
363template<
typename ValueType>
365 switch (elemWithChildren->type()) {
379 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"DFT element type '" << elemWithChildren->type() <<
"' not known.");
384template<
typename ValueType>
387 DFTElementVector& visitedElements) {
388 STORM_LOG_THROW(visited[element] != topoSortColour::GREY, storm::exceptions::WrongFormatException,
"DFT is cyclic.");
389 if (visited[element] == topoSortColour::WHITE) {
391 visited[element] = topoSortColour::GREY;
393 if (element->isGate()) {
394 for (DFTElementPointer
const& child :
std::static_pointer_cast<
storm::dft::storage::elements::DFTGate<ValueType>>(element)->children()) {
396 topologicalVisit(child, visited, visitedElements);
400 else if (element->isRestriction()) {
401 for (DFTElementPointer
const& child :
std::static_pointer_cast<
storm::dft::storage::elements::DFTRestriction<ValueType>>(element)->children()) {
403 topologicalVisit(child, visited, visitedElements);
405 }
else if (element->isDependency()) {
406 for (DFTElementPointer
const& child :
407 std::static_pointer_cast<
storm::dft::storage::elements::DFTDependency<
ValueType>>(element)->dependentEvents()) {
409 topologicalVisit(child, visited, visitedElements);
415 STORM_LOG_ASSERT(element->isBasicElement(),
"Unknown element type " << element->type() <<
" for " << *element);
418 visited[element] = topoSortColour::BLACK;
420 visitedElements.push_back(element);
424template<
typename ValueType>
425bool DFTBuilder<ValueType>::nameInUse(std::string
const& name)
const {
426 return mElements.find(name) != mElements.end();
429template<
typename ValueType>
430bool DFTBuilder<ValueType>::isValidProbability(ValueType value)
const {
439template<
typename ValueType>
440std::vector<std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType>>> DFTBuilder<ValueType>::sortTopological() {
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));
447 DFTElementVector visitedElements;
449 topologicalVisit(mElements[mTopLevelName], visited, visitedElements);
450 for (
auto const& e : visited) {
452 topologicalVisit(e.first, visited, visitedElements);
454 return visitedElements;
457template<
typename ValueType>
458size_t DFTBuilder<ValueType>::computeRank(DFTElementPointer
const& elem) {
459 if (elem->rank() ==
static_cast<decltype(elem-
>rank())>(-1)) {
461 if (elem->isBasicElement() || elem->isDependency() || elem->isRestriction()) {
466 DFTGatePointer gate = std::static_pointer_cast<storm::dft::storage::elements::DFTGate<ValueType>>(elem);
468 for (DFTElementPointer
const& child : gate->children()) {
469 maxRank = std::max(maxRank, computeRank(child));
471 elem->setRank(maxRank + 1);
479template class DFTBuilder<double>;
480template 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)