diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 5d835b4c7..87338ff30 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -87,6 +87,7 @@ void processOptions() { // Apply transformations // TODO transform later before actual analysis dft = storm::api::applyTransformations(*dft, faultTreeSettings.isUniqueFailedBE(), true); + STORM_LOG_DEBUG(dft->getElementsString()); dft->setDynamicBehaviorInfo(); diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index b5ed7c298..1f5f3c18f 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -59,14 +59,14 @@ namespace storm { // Consider all children of the top level gate std::vector isubdft; if (child->nrParents() > 1 || child->hasOutgoingDependencies()) { - STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); + STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation."); isubdft.clear(); } else if (dft.isGate(child->id())) { isubdft = dft.getGate(child->id())->independentSubDft(false); } else { STORM_LOG_ASSERT(dft.isBasicElement(child->id()), "Child is no BE."); if(dft.getBasicElement(child->id())->hasIngoingDependencies()) { - STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); + STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation."); isubdft.clear(); } else { isubdft = {child->id()}; @@ -745,37 +745,35 @@ namespace storm { storm::storage::BitVector coldBEs(subtree.size(), false); for (size_t i = 0; i < subtree.size(); ++i) { size_t id = subtree[i]; + // Consider only still operational BEs if (state->isOperational(id)) { - // Get BE rate - ValueType rate = state->getBERate(id); - if (storm::utility::isZero(rate)) { - // Get active failure rate for cold BE - auto be = dft.getBasicElement(id); - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: - { + auto be = dft.getBasicElement(id); + switch (be->type()) { + case storm::storage::DFTElementType::BE_EXP: + { + // Get BE rate + ValueType rate = state->getBERate(id); + if (storm::utility::isZero(rate)) { + // Get active failure rate for cold BE auto beExp = std::static_pointer_cast const>(be); rate = beExp->activeFailureRate(); STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Failure rate should not be zero."); // Mark BE as cold coldBEs.set(i, true); - break; } - case storm::storage::DFTElementType::BE_CONST: - { - // Ignore BE which cannot fail - continue; - } - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); - break; + rates.push_back(rate); + rateSum += rate; + break; } + case storm::storage::DFTElementType::BE_CONST: + // Ignore BE which cannot fail + continue; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); + break; } - rates.push_back(rate); - rateSum += rate; } } - STORM_LOG_ASSERT(rates.size() > 0, "No rates failable"); // Sort rates diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index daa6c33f2..6b79e1c1e 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -416,7 +416,7 @@ namespace storm { } else { STORM_LOG_ASSERT(isBasicElement(child->id()), "Child is no BE."); if (getBasicElement(child->id())->hasIngoingDependencies()) { - STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); + STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation."); return {*this}; } else { isubdft = {child->id()}; diff --git a/src/storm-dft/storage/dft/elements/BEExponential.h b/src/storm-dft/storage/dft/elements/BEExponential.h index 8347f3179..1ed6221d6 100644 --- a/src/storm-dft/storage/dft/elements/BEExponential.h +++ b/src/storm-dft/storage/dft/elements/BEExponential.h @@ -67,7 +67,8 @@ namespace storm { } bool canFail() const override { - return !storm::utility::isZero(this->activeFailureRate()); + STORM_LOG_ASSERT(!storm::utility::isZero(this->activeFailureRate()), "BEExp should have failure rate > 0"); + return true; } /*! diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index a4ad5fca9..8df237df3 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -156,6 +156,7 @@ namespace storm { // Only perform the assignment if the source and target are not identical. if (this != &other) { bitCount = other.bitCount; + other.bitCount = 0; if (this->buckets) { delete[] this->buckets; }