From 2a4157947691e91caa1ebb0cc6fceecda013e376 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Fri, 26 Feb 2016 14:50:46 +0100
Subject: [PATCH] refactored source file for elements

Former-commit-id: 0315e8a8cb685ef5969664e951593fa372db0918
---
 src/storage/dft/DFTElements.cpp       | 127 --------------------------
 src/storage/dft/elements/DFTBE.h      |   8 +-
 src/storage/dft/elements/DFTElement.h |   5 +-
 src/storage/dft/elements/DFTVot.h     |   1 +
 4 files changed, 11 insertions(+), 130 deletions(-)
 delete mode 100644 src/storage/dft/DFTElements.cpp

diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp
deleted file mode 100644
index 4cf49e0b0..000000000
--- a/src/storage/dft/DFTElements.cpp
+++ /dev/null
@@ -1,127 +0,0 @@
-#include <src/exceptions/NotImplementedException.h>
-#include <src/utility/macros.h>
-#include "DFTElements.h"
-#include "elements/DFTRestriction.h"
-
-namespace storm {
-    namespace storage {
-
-        template<typename ValueType>
-        bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
-            if (state.dontCare(mId)) {
-                return false;
-            }
-            
-            // Check that no outgoing dependencies can be triggered anymore
-            for (DFTDependencyPointer dependency : mOutgoingDependencies) {
-                if (state.isOperational(dependency->dependentEvent()->id()) && state.isOperational(dependency->triggerEvent()->id())) {
-                    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;
-        }
-
-        template<typename ValueType>
-        void DFTElement<ValueType>::extendSpareModule(std::set<size_t>& elementsInModule) const {
-            for(auto const& parent : mParents) {
-                if(elementsInModule.count(parent->id()) == 0 && !parent->isSpareGate()) {
-                    elementsInModule.insert(parent->id());
-                    parent->extendSpareModule(elementsInModule);
-                }
-            }
-        }
-
-        template<typename ValueType>
-        std::vector<size_t> DFTElement<ValueType>::independentUnit() const {
-            std::vector<size_t> res;
-            res.push_back(this->id());
-            // Extend for pdeps.
-            return res;
-        }
-
-        template<typename ValueType>
-        void DFTElement<ValueType>::extendUnit(std::set<size_t>& unit) const {
-            unit.insert(mId);
-        }
-
-        template<typename ValueType>
-        std::vector<size_t> DFTElement<ValueType>::independentSubDft(bool blockParents) const {
-            //std::cout << "INDEPENDENT SUBTREE CALL " << this->id() << std::endl;
-            std::vector<size_t> res;
-            res.push_back(this->id());
-            return res;
-        }
-
-        template<typename ValueType>
-        void DFTElement<ValueType>::extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const {
-            if(elemsInSubtree.count(this->id()) > 0) return;
-            if(std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) {
-                // This is a parent of the suspected root, thus it is not a subdft.
-                elemsInSubtree.clear();
-                return;
-            }
-            elemsInSubtree.insert(mId);
-            for(auto const& parent : mParents) {
-                if(blockParents && std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), parent->id()) != parentsOfSubRoot.end()) {
-                    continue;
-                }
-                parent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
-                if(elemsInSubtree.empty()) {
-                    return;
-                }
-            }
-            for(auto const& dep : mOutgoingDependencies) {
-                dep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
-                if(elemsInSubtree.empty()) {
-                    return;
-                }
-
-            }
-            
-            for(auto const& restr : mRestrictions) {
-                restr->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
-                if(elemsInSubtree.empty()) {
-                    return;
-                }
-            }
-            
-        }
-
-
-        template<typename ValueType>
-        bool DFTBE<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
-            if(DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {
-                state.beNoLongerFailable(this->mId);
-                return true;
-            }
-            return false;
-        }
-
-
-        // Explicitly instantiate the class.
-        template class DFTBE<double>;
-
-#ifdef STORM_HAVE_CARL
-        template class DFTBE<RationalFunction>;
-#endif
-        
-    }
-}
diff --git a/src/storage/dft/elements/DFTBE.h b/src/storage/dft/elements/DFTBE.h
index 5e09e965e..a9c5b030d 100644
--- a/src/storage/dft/elements/DFTBE.h
+++ b/src/storage/dft/elements/DFTBE.h
@@ -93,7 +93,13 @@ namespace storm {
                 return (mActiveFailureRate == otherBE.mActiveFailureRate) && (mPassiveFailureRate == otherBE.mPassiveFailureRate);
             }
             
-            virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override;
+            virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                if(DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {
+                    state.beNoLongerFailable(this->mId);
+                    return true;
+                }
+                return false;
+            }
         };
 
         template<typename ValueType>
diff --git a/src/storage/dft/elements/DFTElement.h b/src/storage/dft/elements/DFTElement.h
index d6840132a..11223f3fa 100644
--- a/src/storage/dft/elements/DFTElement.h
+++ b/src/storage/dft/elements/DFTElement.h
@@ -8,6 +8,7 @@
 #include <set>
 #include <vector>
 #include <memory>
+#include <map>
 
 
 
@@ -204,7 +205,7 @@ namespace storm {
                 return mOutgoingDependencies.size();
             }
             
-            std::set<DFTElement<ValueType>> restrictedItems() const {
+            /*std::set<DFTElement<ValueType>> restrictedItems() const {
                 std::set<DFTElement<ValueType>> result;
                 for(auto const& restr : mRestrictions) {
                     bool foundThis = false;
@@ -236,7 +237,7 @@ namespace storm {
                         }
                     }
                 }
-            }
+            }*/
             
             DFTDependencyVector const& outgoingDependencies() const {
                 return mOutgoingDependencies;
diff --git a/src/storage/dft/elements/DFTVot.h b/src/storage/dft/elements/DFTVot.h
index 3a3e818d2..0233d979d 100644
--- a/src/storage/dft/elements/DFTVot.h
+++ b/src/storage/dft/elements/DFTVot.h
@@ -1,4 +1,5 @@
 #pragma once 
+#include "DFTGate.h"
 namespace storm {
     namespace storage {