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);
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].");
173template<
typename ValueType>
176 if (storm::utility::isZero<ValueType>(rate)) {
177 addBasicElementConst(name,
false);
178 }
else if (phases == 1) {
180 addBasicElementExponential(name, rate, dormancyFactor);
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].");
191template<
typename ValueType>
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.");
199 if (storm::utility::isOne<ValueType>(shape)) {
201 addBasicElementExponential(name, storm::utility::one<ValueType>() / rate, storm::utility::one<ValueType>());
207template<
typename ValueType>
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.");
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 {
432 if (this->comparator.isZero(value) || this->comparator.isOne(value)) {
434 }
else if (!this->comparator.isConstant(value)) {
437 }
else if (this->comparator.isLess(storm::utility::zero<ValueType>(), value) && this->comparator.isLess(value, storm::utility::one<ValueType>())) {
443template<
typename ValueType>
444std::vector<std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType>>> DFTBuilder<ValueType>::sortTopological() {
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));
451 DFTElementVector visitedElements;
453 topologicalVisit(mElements[mTopLevelName], visited, visitedElements);
454 for (
auto const& e : visited) {
456 topologicalVisit(e.first, visited, visitedElements);
458 return visitedElements;
461template<
typename ValueType>
462size_t DFTBuilder<ValueType>::computeRank(DFTElementPointer
const& elem) {
463 if (elem->rank() ==
static_cast<decltype(elem-
>rank())>(-1)) {
465 if (elem->isBasicElement() || elem->isDependency() || elem->isRestriction()) {
470 DFTGatePointer gate = std::static_pointer_cast<storm::dft::storage::elements::DFTGate<ValueType>>(elem);
472 for (DFTElementPointer
const& child : gate->children()) {
473 maxRank = std::max(maxRank, computeRank(child));
475 elem->setRank(maxRank + 1);
483template class DFTBuilder<double>;
484template class DFTBuilder<RationalFunction>;