diff --git a/examples/dft/spare8.dft b/examples/dft/spare8.dft new file mode 100644 index 000000000..c67eaf022 --- /dev/null +++ b/examples/dft/spare8.dft @@ -0,0 +1,7 @@ +toplevel "A"; +"A" wsp "I" "B"; +"B" wsp "J" "K"; +"I" lambda=0.5 dorm=0.3; +"J" lambda=0.5 dorm=0.3; +"K" lambda=0.5 dorm=0.3; + diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index cbb9b69d0..4900845a5 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -256,7 +256,7 @@ namespace storm { if (mStates.contains(unsuccessfulState->status())) { // Unsuccessful state already exists unsuccessfulStateId = mStates.getValue(unsuccessfulState->status()); - STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " already exists"); + STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " with id " << unsuccessfulStateId << " already exists"); } else { // New unsuccessful state unsuccessfulState->setId(newIndex++); @@ -277,16 +277,15 @@ namespace storm { ++rowOffset; } else { - // Set failure rate according to usage - bool isUsed = true; + // Set failure rate according to activation + bool isActive = true; if (mDft.hasRepresentant(nextBE->id())) { - DFTElementCPointer representant = mDft.getRepresentant(nextBE->id()); - // Used must be checked for the state we are coming from as this state is responsible for the + // Active must be checked for the state we are coming from as this state is responsible for the // rate and not the new state we are going to - isUsed = state->isUsed(representant->id()); + isActive = state->isActive(mDft.getRepresentant(nextBE->id())->id()); } - STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used")); - ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); + STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isActive ? "active" : "not active")); + ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); auto resultFind = outgoingTransitions.find(newStateId); if (resultFind != outgoingTransitions.end()) { // Add to existing transition diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 92e780872..3fbcd5ee1 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -191,10 +191,11 @@ namespace storm { } else { stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id())); if(elem->isSpareGate()) { - if(state->isActiveSpare(elem->id())) { - stream << " actively"; + size_t useId = state->uses(elem->id()); + if(state->isActive(useId)) { + stream << " actively "; } - stream << " using " << state->uses(elem->id()); + stream << " using " << useId; } } stream << std::endl; @@ -214,10 +215,11 @@ namespace storm { stream << storm::storage::toChar(state->getElementState(elem->id())); if(elem->isSpareGate()) { stream << "["; - if(state->isActiveSpare(elem->id())) { - stream << "actively "; + size_t useId = state->uses(elem->id()); + if(state->isActive(useId)) { + stream << " actively "; } - stream << "using " << state->uses(elem->id()) << "]"; + stream << "using " << useId << "]"; } } } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index eaee1d54a..22c819f84 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -259,11 +259,13 @@ namespace storm { virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; virtual void extendSpareModule(std::set& elementsInSpareModule) const override { - DFTElement::extendSpareModule(elementsInSpareModule); - for(auto const& child : mChildren) { - if(elementsInSpareModule.count(child->id()) == 0) { - elementsInSpareModule.insert(child->id()); - child->extendSpareModule(elementsInSpareModule); + if (!this->isSpareGate()) { + DFTElement::extendSpareModule(elementsInSpareModule); + for( auto const& child : mChildren) { + if(elementsInSpareModule.count(child->id()) == 0) { + elementsInSpareModule.insert(child->id()); + child->extendSpareModule(elementsInSpareModule); + } } } } @@ -350,6 +352,9 @@ namespace storm { } } state.setFailed(this->mId); + if (this->isSpareGate()) { + this->finalizeSpare(state); + } this->childrenDontCare(state, queues); } @@ -360,6 +365,9 @@ namespace storm { } } state.setFailsafe(this->mId); + if (this->isSpareGate()) { + this->finalizeSpare(state); + } this->childrenDontCare(state, queues); } @@ -367,6 +375,20 @@ namespace storm { queues.propagateDontCare(mChildren); } + /** + * Finish failed/failsafe spare gate by activating the children and setting the useIndex to zero. + * This prevents multiple fail states with different usages or activations. + * @param state The current state. + */ + void finalizeSpare(DFTState& state) const { + state.setUses(this->mId, 0); + for (auto child : this->children()) { + if (!state.isActive(child->id())) { + state.activate(child->id()); + } + } + } + bool hasFailsafeChild(DFTState& state) const { for(auto const& child : mChildren) { if(state.isFailsafe(child->id())) diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 0bad03f78..7f34e03ef 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -7,7 +7,6 @@ namespace storm { template DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { - mInactiveSpares = dft.getSpareIndices(); // Initialize uses for(size_t id : mDft.getSpareIndices()) { @@ -18,12 +17,7 @@ namespace storm { } // Initialize activation - this->activate(mDft.getTopLevelIndex()); - for(auto const& id : mDft.module(mDft.getTopLevelIndex())) { - if(mDft.getElement(id)->isSpareGate()) { - propagateActivation(uses(id)); - } - } + propagateActivation(mDft.getTopLevelIndex()); std::vector alwaysActiveBEs = dft.nonColdBEs(); mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); @@ -182,29 +176,25 @@ namespace storm { template void DFTState::activate(size_t repr) { - for(size_t elem : mDft.module(repr)) { - if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) { - mIsCurrentlyFailableBE.push_back(elem); - } - else if(mDft.getElement(elem)->isSpareGate()) { - assert(std::find(mInactiveSpares.begin(), mInactiveSpares.end(), elem) != mInactiveSpares.end()); - mInactiveSpares.erase(std::find(mInactiveSpares.begin(), mInactiveSpares.end(), elem)); - } - } + size_t activationIndex = mStateGenerationInfo.getSpareActivationIndex(repr); + assert(!mStatus[activationIndex]); + mStatus.set(activationIndex); + propagateActivation(repr); } template - bool DFTState::isActiveSpare(size_t id) const { - assert(mDft.getElement(id)->isSpareGate()); - return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end()); + bool DFTState::isActive(size_t id) const { + assert(mDft.isRepresentative(id)); + return mStatus[mStateGenerationInfo.getSpareActivationIndex(id)]; } template void DFTState::propagateActivation(size_t representativeId) { - activate(representativeId); - for(size_t id : mDft.module(representativeId)) { - if(mDft.getElement(id)->isSpareGate()) { - propagateActivation(uses(id)); + for(size_t elem : mDft.module(representativeId)) { + if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) { + mIsCurrentlyFailableBE.push_back(elem); + } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) { + activate(uses(elem)); } } } @@ -243,8 +233,8 @@ namespace storm { size_t childId = (*it)->id(); if(!hasFailed(childId) && !isUsed(childId)) { setUses(spareId, childId); - if(isActiveSpare(spareId)) { - propagateActivation(childId); + if(isActive(currentlyUses)) { + activate(childId); } return true; } diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 821aa2fcb..7a26e10ab 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -26,7 +26,6 @@ namespace storm { // Status is bitvector where each element has two bits with the meaning according to DFTElementState storm::storage::BitVector mStatus; size_t mId; - std::vector mInactiveSpares; std::vector mIsCurrentlyFailableBE; std::vector mFailableDependencies; std::vector mUsedRepresentants; @@ -79,9 +78,7 @@ namespace storm { void activate(size_t repr); - bool isActiveSpare(size_t id) const; - - void propagateActivation(size_t representativeId); + bool isActive(size_t id) const; void markAsInvalid() { mValid = false; @@ -200,6 +197,10 @@ namespace storm { friend bool operator==(DFTState const& a, DFTState const& b) { return a.mStatus == b.mStatus; } + + private: + void propagateActivation(size_t representativeId); + }; }