diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 7f3e8c09e..28b943ba9 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -522,9 +522,6 @@ namespace storm { for (size_t index = 0; index < state->nrFailableBEs(); ++index) { lowerBound += state->getFailableBERate(index); } - for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { - lowerBound += state->getNotFailableBERate(index); - } return lowerBound; } @@ -538,20 +535,31 @@ namespace storm { for (std::vector const& subtree : subtreeBEs) { // Get all possible rates std::vector rates; - for (size_t id : subtree) { + storm::storage::BitVector coldBEs(subtree.size(), false); + for (size_t i = 0; i < subtree.size(); ++i) { + size_t id = subtree[i]; if (state->isOperational(id)) { // Get BE rate - rates.push_back(state->getBERate(id, true)); - rateSum += rates.back(); + ValueType rate = state->getBERate(id); + if (storm::utility::isZero(rate)) { + // Get active failure rate for cold BE + rate = dft.getBasicElement(id)->activeFailureRate(); + // Mark BE as cold + coldBEs.set(i, true); + } + rates.push_back(rate); + rateSum += rate; } } - // We move backwards and start with swapping the last element to itself - // Then we do not need to swap back - for (auto it = rates.rbegin(); it != rates.rend(); ++it) { - // Compute AND MTTF of subtree without current rate and scale with current rate - std::iter_swap(it, rates.end() - 1); - upperBound += rates.back() * computeMTTFAnd(rates, rates.size() - 1); + for (size_t i = 0; i < rates.size(); ++i) { + // Cold BEs cannot fail in the first step + if (!coldBEs.get(i)) { + // Compute AND MTTF of subtree without current rate and scale with current rate + upperBound += rates.back() * computeMTTFAnd(rates, rates.size() - 1); + // Swap here to avoid swapping back + std::iter_swap(rates.begin() + i, rates.end() - 1); + } } } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 64728cbd5..cc0eaabec 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -17,23 +17,11 @@ namespace storm { this->setUses(spareId, elem->children()[0]->id()); } - for (auto elem : mDft.getBasicElements()) { - if (!storm::utility::isZero(elem->activeFailureRate())) { - mCurrentlyNotFailableBE.push_back(elem->id()); - } - } - // Initialize activation propagateActivation(mDft.getTopLevelIndex()); std::vector alwaysActiveBEs = mDft.nonColdBEs(); mCurrentlyFailableBE.insert(mCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); - // Remove always active BEs from currently not failable BEs - for (size_t id : alwaysActiveBEs) { - auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), id); - STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Id not found."); - mCurrentlyNotFailableBE.erase(it); - } } template @@ -46,7 +34,6 @@ namespace storm { STORM_LOG_TRACE("Construct concrete state from pseudo state " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); // Clear information from pseudo state mCurrentlyFailableBE.clear(); - mCurrentlyNotFailableBE.clear(); mFailableDependencies.clear(); mUsedRepresentants.clear(); STORM_LOG_ASSERT(mPseudoState, "Only pseudo states can be constructed."); @@ -57,10 +44,6 @@ namespace storm { if ((!be->isColdBasicElement() && be->canFail()) || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) { mCurrentlyFailableBE.push_back(index); STORM_LOG_TRACE("Currently failable: " << mDft.getBasicElement(index)->toString()); - } else { - // BE currently is not failable - mCurrentlyNotFailableBE.push_back(index); - STORM_LOG_TRACE("Currently not failable: " << mDft.getBasicElement(index)->toString()); } } else if (mDft.getElement(index)->isSpareGate()) { // Initialize used representants @@ -204,11 +187,6 @@ namespace storm { auto it = std::find(mCurrentlyFailableBE.begin(), mCurrentlyFailableBE.end(), id); if (it != mCurrentlyFailableBE.end()) { mCurrentlyFailableBE.erase(it); - } else { - it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), id); - if (it != mCurrentlyNotFailableBE.end()) { - mCurrentlyNotFailableBE.erase(it); - } } } @@ -241,35 +219,22 @@ namespace storm { } template - ValueType DFTState::getBERate(size_t id, bool avoidCold) const { + ValueType DFTState::getBERate(size_t id) const { STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE."); if (mDft.hasRepresentant(id) && !isActive(mDft.getRepresentant(id))) { - if (avoidCold && mDft.getBasicElement(id)->isColdBasicElement()) { - // Return active failure rate instead of 0. - return mDft.getBasicElement(id)->activeFailureRate(); - } else { - // Return passive failure rate - return mDft.getBasicElement(id)->passiveFailureRate(); - } + // Return passive failure rate + return mDft.getBasicElement(id)->passiveFailureRate(); + } else { + // Return active failure rate + return mDft.getBasicElement(id)->activeFailureRate(); } - // Return active failure rate - return mDft.getBasicElement(id)->activeFailureRate(); } template ValueType DFTState::getFailableBERate(size_t index) const { STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid."); - return getBERate(mCurrentlyFailableBE[index], false); - } - - template - ValueType DFTState::getNotFailableBERate(size_t index) const { - STORM_LOG_ASSERT(index < nrNotFailableBEs(), "Index invalid."); - STORM_LOG_ASSERT(isPseudoState() || storm::utility::isZero(mDft.getBasicElement(mCurrentlyNotFailableBE[index])->activeFailureRate()) || - (mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail in state: " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); - // Use active failure rate as passive failure rate is 0. - return getBERate(mCurrentlyNotFailableBE[index], true); + return getBERate(mCurrentlyFailableBE[index]); } template @@ -326,10 +291,6 @@ namespace storm { if (be->isColdBasicElement() && be->canFail()) { // Add to failable BEs mCurrentlyFailableBE.push_back(elem); - // Remove from not failable BEs - auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), elem); - STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element " << elem << " not found."); - mCurrentlyNotFailableBE.erase(it); } } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) { propagateActivation(uses(elem)); diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 0f8280591..b077b58b0 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -27,7 +27,6 @@ namespace storm { storm::storage::BitVector mStatus; size_t mId; std::vector mCurrentlyFailableBE; - std::vector mCurrentlyNotFailableBE; std::vector mFailableDependencies; std::vector mUsedRepresentants; bool mPseudoState; @@ -181,15 +180,6 @@ namespace storm { return mCurrentlyFailableBE.size(); } - /** - * Get number of currently not failable BEs. These are cold BE which can fail in the future. - * - * @return Number of not failable BEs. - */ - size_t nrNotFailableBEs() const { - return mCurrentlyNotFailableBE.size(); - } - /** * Get the failure rate of the currently failable BE on the given index. * @@ -200,24 +190,13 @@ namespace storm { ValueType getFailableBERate(size_t index) const; /** - * Get the failure rate of the currently not failable BE on the given index. - * - * @param index Index of BE in list of currently not failable BEs. - * - * @return Failure rate of the BE. - */ - ValueType getNotFailableBERate(size_t index) const; - - /** - * Get the failure rate of the given BE. + * Get the current failure rate of the given BE. * * @param id Id of BE. - * @param avoidCold Flag indicating if a cold passive failure rate should be avoided by giving - * the active failure rate instead. * * @return Failure rate of the BE. */ - ValueType getBERate(size_t id, bool avoidCold) const; + ValueType getBERate(size_t id) const; /** Get number of currently failable dependencies. *