Finalize sparse for failed, failsafe, dontcare

Former-commit-id: 722285c8d5

src/storage/dft/DFTElements.cpp

@@ -17,17 +17,24 @@ namespace storm {
                     return false;
                 }
             }
+            
+            bool hasParentSpare = false;
+
             // Check that no parent can fail anymore
             for(DFTGatePointer const& parent : mParents) {
                 if(state.isOperational(parent->id())) {
                     return false;
                 }
+                if (parent->isSpareGate()) {
+                    hasParentSpare = true;
+                }
             }
             
-            
-        
-
             state.setDontCare(mId);
+            if (hasParentSpare && !state.isActive(mId)) {
+                // Activate child for consistency in failed spares
+                state.activate(mId);
+            }
             return true;
         }
 

src/storage/dft/DFTElements.h

@@ -387,10 +387,6 @@ namespace storm {
                     queues.checkRestrictionLater(restr);
                 }
                 state.setFailed(this->mId);
-                // TODO can this be moved towards DFTSpare?
-                if (this->isSpareGate()) {
-                    this->finalizeSpare(state);
-                }
                 this->childrenDontCare(state, queues);
             }
 
@@ -401,30 +397,13 @@ namespace storm {
                     }
                 }
                 state.setFailsafe(this->mId);
-                if (this->isSpareGate()) {
-                    this->finalizeSpare(state);
-                }
                 this->childrenDontCare(state, queues);
             }
-
+            
             void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
                 queues.propagateDontCare(mChildren);
             }
 
-            /**
-             * Finish failed/failsafe spare gate by activating the children and setting the useIndex to the maximum value.
-             * This prevents multiple fail states with different usages or activations.
-             * @param state The current state.
-             */
-            void finalizeSpare(DFTState<ValueType>& state) const {
-                state.finalizeUses(this->mId);
-                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()))
@@ -959,6 +938,24 @@ namespace storm {
                 return true;
             }
             
+            void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                DFTGate<ValueType>::fail(state, queues);
+                state.finalizeUses(this->mId);
+            }
+            
+            void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                DFTGate<ValueType>::failsafe(state, queues);
+                state.finalizeUses(this->mId);
+            }
+            
+            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                if (DFTGate<ValueType>::checkDontCareAnymore(state, queues)) {
+                    state.finalizeUses(this->mId);
+                    return true;
+                }
+                return false;
+            }
+            
             void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 if(state.isOperational(this->mId)) {
                     size_t uses = state.uses(this->mId);
@@ -979,6 +976,7 @@ namespace storm {
                     }
                 }
             }
+
         };
         
         template<typename ValueType>

src/storage/dft/DFTState.cpp

@@ -179,7 +179,6 @@ namespace storm {
             size_t activationIndex = mStateGenerationInfo.getSpareActivationIndex(repr);
             assert(!mStatus[activationIndex]);
             mStatus.set(activationIndex);
-            propagateActivation(repr);
         }
 
         template<typename ValueType>
@@ -190,11 +189,14 @@ namespace storm {
             
         template<typename ValueType>
         void DFTState<ValueType>::propagateActivation(size_t representativeId) {
+            if (representativeId != mDft.getTopLevelIndex()) {
+                activate(representativeId);
+            }
             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));
+                    propagateActivation(uses(elem));
                 }
             }
         }
@@ -245,7 +247,7 @@ namespace storm {
                 if(!hasFailed(childId) && !isUsed(childId)) {
                     setUses(spareId, childId);
                     if(isActive(currentlyUses)) {
-                        activate(childId);
+                        propagateActivation(childId);
                     }
                     return true;
                 }