From 98b628b269c4a0de69a419a1c07f8fef9d31d420 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 16 Dec 2018 22:48:37 +0100 Subject: [PATCH] Moved failableBE/Dependencies to own struct --- .../builder/ExplicitDFTModelBuilder.cpp | 6 +- .../generator/DftNextStateGenerator.cpp | 25 +-- src/storm-dft/storage/dft/DFTState.cpp | 62 +++---- src/storm-dft/storage/dft/DFTState.h | 157 +++++++++++++----- 4 files changed, 153 insertions(+), 97 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 87cec9ce8..466cba537 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -387,7 +387,7 @@ namespace storm { // Initialize heuristic values ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); iter->second.second = heuristic; - if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) { + if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && state->getFailableElements().hasBEs())) { // Do not skip absorbing state or if reached by dependencies iter->second.second->markExpand(); } @@ -642,8 +642,8 @@ namespace storm { ValueType ExplicitDFTModelBuilder::getLowerBound(DFTStatePointer const& state) const { // Get the lower bound by considering the failure of all possible BEs ValueType lowerBound = storm::utility::zero(); - for (size_t index = 0; index < state->nrFailableBEs(); ++index) { - lowerBound += state->getFailableBERate(index); + for (state->getFailableElements().init(false); !state->getFailableElements().isEnd(); state->getFailableElements().next()) { + lowerBound += state->getBERate(state->getFailableElements().get()); } return lowerBound; } diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 004aabccc..2a3502c5e 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -51,12 +51,13 @@ namespace storm { StateBehavior result; // Initialization - bool hasDependencies = state->nrFailableDependencies() > 0; - size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); - size_t currentFailable = 0; + bool hasDependencies = state->getFailableElements().hasDependencies(); + //size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); + //size_t currentFailable = 0; + state->getFailableElements().init(hasDependencies); // Check for absorbing state - if (mDft.hasFailed(state) || mDft.isFailsafe(state) || failableCount == 0) { + if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->getFailableElements().isEnd()) { Choice choice(0, true); // Add self loop choice.addProbability(state->getId(), storm::utility::one()); @@ -70,16 +71,18 @@ namespace storm { Choice choice(0, !hasDependencies); // Let BE fail - while (currentFailable < failableCount) { - if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && currentFailable > 0) { + bool isFirst = true; + while (!state->getFailableElements().isEnd()) { + if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && !isFirst) { // We discard further exploration as we already chose one dependent event break; } STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed."); + isFirst = false; // Construct new state as copy from original one DFTStatePointer newState = state->copy(); - std::pair const>, bool> nextBEPair = newState->letNextBEFail(currentFailable); + std::pair const>, bool> nextBEPair = newState->letNextBEFail(state->getFailableElements().get()); std::shared_ptr const>& nextBE = nextBEPair.first; STORM_LOG_ASSERT(nextBE, "NextBE is null."); STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match."); @@ -114,7 +117,7 @@ namespace storm { if(newState->isInvalid() || (nextBE->isTransient() && !newState->hasFailed(mDft.getTopLevelIndex()))) { // Continue with next possible state - ++currentFailable; + state->getFailableElements().next(); STORM_LOG_TRACE("State is ignored because " << (newState->isInvalid() ? "it is invalid" : "the transient fault is ignored")); continue; } @@ -148,14 +151,14 @@ namespace storm { // Set transitions if (hasDependencies) { // Failure is due to dependency -> add non-deterministic choice - ValueType probability = mDft.getDependency(state->getDependencyId(currentFailable))->probability(); + ValueType probability = mDft.getDependency(state->getFailableElements().get())->probability(); choice.addProbability(newStateId, probability); STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << probability); if (!storm::utility::isOne(probability)) { // Add transition to state where dependency was unsuccessful DFTStatePointer unsuccessfulState = state->copy(); - unsuccessfulState->letDependencyBeUnsuccessful(currentFailable); + unsuccessfulState->letDependencyBeUnsuccessful(state->getFailableElements().get()); // Add state StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState); ValueType remainingProbability = storm::utility::one() - probability; @@ -179,7 +182,7 @@ namespace storm { } STORM_LOG_ASSERT(newStateId != state->getId(), "Self loop was added for " << newStateId << " and failure of " << nextBE->name()); - ++currentFailable; + state->getFailableElements().next(); } // end while failing BE if (!hasDependencies) { diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index d6a1794af..26d3c42da 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -6,7 +6,7 @@ namespace storm { namespace storage { template - DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateBitVectorSize()), mId(id), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { + DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateBitVectorSize()), mId(id), failableElements(dft.nrElements()), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { // TODO Matthias: use construct() // Initialize uses @@ -20,12 +20,14 @@ namespace storm { // Initialize activation propagateActivation(mDft.getTopLevelIndex()); - std::vector alwaysActiveBEs = mDft.nonColdBEs(); - mCurrentlyFailableBE.insert(mCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); + // Initialize currently failable BEs + for (size_t id : mDft.nonColdBEs()) { + failableElements.addBE(id); + } } template - DFTState::DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { + DFTState::DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), failableElements(dft.nrElements()), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { // Intentionally left empty } @@ -33,8 +35,7 @@ namespace storm { void DFTState::construct() { STORM_LOG_TRACE("Construct concrete state from pseudo state " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); // Clear information from pseudo state - mCurrentlyFailableBE.clear(); - mFailableDependencies.clear(); + failableElements.clear(); mUsedRepresentants.clear(); STORM_LOG_ASSERT(mPseudoState, "Only pseudo states can be constructed."); for(size_t index = 0; index < mDft.nrElements(); ++index) { @@ -42,7 +43,7 @@ namespace storm { if (mDft.isBasicElement(index) && isOperational(index)) { std::shared_ptr> be = mDft.getBasicElement(index); if (be->canFail() && (!be->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index)))) { - mCurrentlyFailableBE.push_back(index); + failableElements.addBE(index); STORM_LOG_TRACE("Currently failable: " << be->toString()); } } else if (mDft.getElement(index)->isSpareGate()) { @@ -59,7 +60,7 @@ namespace storm { STORM_LOG_ASSERT(dependencyId == dependency->id(), "Ids do not match."); assert(dependency->dependentEvents().size() == 1); if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) { - mFailableDependencies.push_back(dependencyId); + failableElements.addDependency(dependencyId); STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); } } @@ -185,10 +186,7 @@ namespace storm { template void DFTState::beNoLongerFailable(size_t id) { - auto it = std::find(mCurrentlyFailableBE.begin(), mCurrentlyFailableBE.end(), id); - if (it != mCurrentlyFailableBE.end()) { - mCurrentlyFailableBE.erase(it); - } + failableElements.removeBE(id); } template @@ -202,13 +200,11 @@ namespace storm { assert(dependency->dependentEvents().size() == 1); if (getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) { STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvents()[0]->id()), "Dependent event is failsafe."); - if (std::find(mFailableDependencies.begin(), mFailableDependencies.end(), dependency->id()) == mFailableDependencies.end()) { - mFailableDependencies.push_back(dependency->id()); - STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); - } + failableElements.addDependency(dependency->id()); + STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); } } - return nrFailableDependencies() > 0; + return failableElements.hasDependencies(); } template @@ -237,43 +233,35 @@ namespace storm { } template - ValueType DFTState::getFailableBERate(size_t index) const { - STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid."); - return getBERate(mCurrentlyFailableBE[index]); - } - - template - std::pair const>, bool> DFTState::letNextBEFail(size_t index) { + std::pair const>, bool> DFTState::letNextBEFail(size_t id) { STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); - if (nrFailableDependencies() > 0) { + if (failableElements.hasDependencies()) { // Consider failure due to dependency - STORM_LOG_ASSERT(index < nrFailableDependencies(), "Index invalid."); - std::shared_ptr const> dependency = mDft.getDependency(mFailableDependencies[index]); - assert(dependency->dependentEvents().size() == 1); + std::shared_ptr const> dependency = mDft.getDependency(id); + STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "More than one dependent event"); std::pair const>,bool> res(mDft.getBasicElement(dependency->dependentEvents()[0]->id()), true); STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << res.first->toString() << " has already failed."); - mFailableDependencies.erase(mFailableDependencies.begin() + index); + failableElements.removeDependency(id); setFailed(res.first->id()); setDependencySuccessful(dependency->id()); beNoLongerFailable(res.first->id()); return res; } else { // Consider "normal" failure - STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid."); - std::pair const>,bool> res(mDft.getBasicElement(mCurrentlyFailableBE[index]), false); + std::pair const>,bool> res(mDft.getBasicElement(id), false); STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << res.first->toString() << " has already failed."); STORM_LOG_ASSERT(res.first->canFail(), "Element " << *(res.first) << " cannot fail."); - mCurrentlyFailableBE.erase(mCurrentlyFailableBE.begin() + index); + failableElements.removeBE(id); setFailed(res.first->id()); return res; } } template - void DFTState::letDependencyBeUnsuccessful(size_t index) { - STORM_LOG_ASSERT(nrFailableDependencies() > 0 && index < nrFailableDependencies(), "Index invalid."); - std::shared_ptr const> dependency = mDft.getDependency(getDependencyId(index)); - mFailableDependencies.erase(mFailableDependencies.begin() + index); + void DFTState::letDependencyBeUnsuccessful(size_t id) { + STORM_LOG_ASSERT(failableElements.hasDependencies(), "Index invalid."); + std::shared_ptr const> dependency = mDft.getDependency(id); + failableElements.removeDependency(id); setDependencyUnsuccessful(dependency->id()); } @@ -299,7 +287,7 @@ namespace storm { std::shared_ptr> be = mDft.getBasicElement(elem); if (be->isColdBasicElement() && be->canFail()) { // Add to failable BEs - mCurrentlyFailableBE.push_back(elem); + failableElements.addBE(elem); } } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) { propagateActivation(uses(elem)); diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index 4dfcf3a13..427115de4 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -22,12 +22,102 @@ namespace storm { template class DFTState { friend struct std::hash; + + struct FailableElements { + + FailableElements(size_t nrElements) : currentlyFailableBE(nrElements), it(currentlyFailableBE.begin()) { + // Intentionally left empty + } + + void addBE(size_t id) { + currentlyFailableBE.set(id); + } + + void addDependency(size_t id) { + if (std::find(mFailableDependencies.begin(), mFailableDependencies.end(), id) == mFailableDependencies.end()) { + mFailableDependencies.push_back(id); + } + } + + void removeBE(size_t id) { + currentlyFailableBE.set(id, false); + } + + void removeDependency(size_t id) { + auto it = std::find(mFailableDependencies.begin(), mFailableDependencies.end(), id); + if (it != mFailableDependencies.end()) { + mFailableDependencies.erase(it); + } + } + + void clear() { + currentlyFailableBE.clear(); + mFailableDependencies.clear(); + } + + void init(bool dependency) const { + this->dependency = dependency; + if (this->dependency) { + itDep = mFailableDependencies.begin(); + } else { + it = currentlyFailableBE.begin(); + } + } + + /** + * Increment iterator. + */ + void next() const { + if (dependency) { + ++itDep; + } else { + ++it; + } + } + + bool isEnd() const { + if (dependency) { + return itDep == mFailableDependencies.end(); + } else { + return it == currentlyFailableBE.end(); + } + } + + /** + * Get underlying element of iterator. + * @return Id of element. + */ + size_t get() const { + if (dependency) { + return *itDep; + } else { + return *it; + } + }; + + bool hasDependencies() const { + return !mFailableDependencies.empty(); + } + + bool hasBEs() const { + return !currentlyFailableBE.empty(); + } + + mutable bool dependency; + + storm::storage::BitVector currentlyFailableBE; + std::vector mFailableDependencies; + + mutable storm::storage::BitVector::const_iterator it; + mutable std::vector::const_iterator itDep; + }; + + private: // Status is bitvector where each element has two bits with the meaning according to DFTElementState storm::storage::BitVector mStatus; size_t mId; - std::vector mCurrentlyFailableBE; - std::vector mFailableDependencies; + FailableElements failableElements; std::vector mUsedRepresentants; bool mPseudoState; bool mValid = true; @@ -124,6 +214,10 @@ namespace storm { storm::storage::BitVector const& status() const { return mStatus; } + + FailableElements& getFailableElements() { + return failableElements; + } /** * This method returns the id of the used child for a spare. If no element is used, it returns the given id. @@ -170,15 +264,6 @@ namespace storm { * @return True, if claiming was successful. */ bool claimNew(size_t spareId, size_t currentlyUses, std::vector>> const& children); - - /** - * Get number of currently failable BEs. - * - * @return Number of failable BEs. - */ - size_t nrFailableBEs() const { - return mCurrentlyFailableBE.size(); - } /** * Get the failure rate of the currently failable BE on the given index. @@ -198,24 +283,6 @@ namespace storm { */ ValueType getBERate(size_t id) const; - /** Get number of currently failable dependencies. - * - * @return Number of failable dependencies. - */ - size_t nrFailableDependencies() const { - return mFailableDependencies.size(); - } - - /** - * Gets the id of the dependency at index in the list of failable dependencies. - * @param index Index in list of failable dependencies. - * @return Id of the dependency - */ - size_t getDependencyId(size_t index) const { - STORM_LOG_ASSERT(index < nrFailableDependencies(), "Index invalid."); - return mFailableDependencies[index]; - } - /** * Sets all failable BEs due to dependencies from newly failed element * @param id Id of the newly failed element @@ -257,28 +324,26 @@ namespace storm { std::string getCurrentlyFailableString() const { std::stringstream stream; - if (nrFailableDependencies() > 0) { - auto it = mFailableDependencies.begin(); + if (failableElements.hasDependencies()) { + failableElements.init(true); stream << "{Dependencies: "; - if (it != mFailableDependencies.end()) { - stream << *it; - } - ++it; - while(it != mFailableDependencies.end()) { - stream << ", " << *it; - ++it; + stream << failableElements.get(); + failableElements.next(); + while(!failableElements.isEnd()) { + stream << ", " << failableElements.get(); + failableElements.next(); } stream << "} "; } else { - auto it = mCurrentlyFailableBE.begin(); + failableElements.init(false); stream << "{"; - if(it != mCurrentlyFailableBE.end()) { - stream << *it; - } - ++it; - while(it != mCurrentlyFailableBE.end()) { - stream << ", " << *it; - ++it; + if (!failableElements.isEnd()) { + stream << failableElements.get(); + failableElements.next(); + while (!failableElements.isEnd()) { + stream << ", " << failableElements.get(); + failableElements.next(); + } } stream << "}"; }