From 9c30394b33ce72e4a7b467743910061ae8c49d09 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Thu, 25 Feb 2016 14:59:27 +0100
Subject: [PATCH] Finalize sparse for failed, failsafe, dontcare

Former-commit-id: 722285c8d5e4c4d350ae56150bb287f1c8c5d298
---
 src/storage/dft/DFTElements.cpp | 13 +++++++---
 src/storage/dft/DFTElements.h   | 42 ++++++++++++++++-----------------
 src/storage/dft/DFTState.cpp    |  8 ++++---
 3 files changed, 35 insertions(+), 28 deletions(-)

diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp
index 7bb8c2cf5..3f1d30017 100644
--- a/src/storage/dft/DFTElements.cpp
+++ b/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;
         }
 
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index 48318d0ae..0b970355f 100644
--- a/src/storage/dft/DFTElements.h
+++ b/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>
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index 8af84255c..7d3b25c8a 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/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;
                 }