Fixed activation of spares

Former-commit-id: f62ccdc79a

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;
+

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

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 << "]";
                     }
                 }
             }

src/storage/dft/DFTElements.h

@@ -259,11 +259,13 @@ namespace storm {
             virtual void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
             
             virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
-                DFTElement<ValueType>::extendSpareModule(elementsInSpareModule);
-                for(auto const& child : mChildren) {
-                    if(elementsInSpareModule.count(child->id()) == 0) {
-                        elementsInSpareModule.insert(child->id());
-                        child->extendSpareModule(elementsInSpareModule);
+                if (!this->isSpareGate()) {
+                    DFTElement<ValueType>::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<ValueType>& state) const {
+                state.setUses(this->mId, 0);
+                for (auto child : this->children()) {
+                    if (!state.isActive(child->id())) {
+                        state.activate(child->id());
+                    }
+                }
+            }
+
             bool hasFailsafeChild(DFTState<ValueType>& state) const {
                 for(auto const& child : mChildren) {
                     if(state.isFailsafe(child->id()))

src/storage/dft/DFTState.cpp

@@ -7,7 +7,6 @@ namespace storm {
 
         template<typename ValueType>
         DFTState<ValueType>::DFTState(DFT<ValueType> 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<size_t> alwaysActiveBEs = dft.nonColdBEs();
             mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
@@ -182,29 +176,25 @@ namespace storm {
 
         template<typename ValueType>
         void DFTState<ValueType>::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<typename ValueType>
-        bool DFTState<ValueType>::isActiveSpare(size_t id) const {
-            assert(mDft.getElement(id)->isSpareGate());
-            return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end());
+        bool DFTState<ValueType>::isActive(size_t id) const {
+            assert(mDft.isRepresentative(id));
+            return mStatus[mStateGenerationInfo.getSpareActivationIndex(id)];
         }
             
         template<typename ValueType>
         void DFTState<ValueType>::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;
                 }

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<size_t> mInactiveSpares;
             std::vector<size_t> mIsCurrentlyFailableBE;
             std::vector<size_t> mFailableDependencies;
             std::vector<size_t> 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);
+
         };
 
     }