From 2754450f91d26079332baed8d89d1d98cc0b3e90 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Fri, 19 Feb 2016 15:47:57 +0100
Subject: [PATCH] Refactored DFS search into own method

Former-commit-id: 3efbcf062f6928f318d91347f3d2eb1eb9946049
---
 src/storage/dft/DFT.cpp | 74 ++++++++++++++++++++++-------------------
 src/storage/dft/DFT.h   |  2 ++
 2 files changed, 41 insertions(+), 35 deletions(-)

diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index 522173d81..c75d96a6c 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -82,43 +82,12 @@ namespace storm {
             visitQueue.push(subTreeRoots[0]);
             bool consideredDependencies = false;
             while (true) {
-                while (!visitQueue.empty()) {
-                    size_t id = visitQueue.front();
-                    visitQueue.pop();
-                    if (visited.count(id) == 1) {
-                        // Already visited
-                        continue;
-                    }
-                    visited.insert(id);
-                    DFTElementPointer element = mElements[id];
-                    
-                    // Insert children
-                    if (element->isGate()) {
-                        for (auto const& child : std::static_pointer_cast<DFTGate<ValueType>>(element)->children()) {
-                            visitQueue.push(child->id());
-                        }
-                    }
-                    
-                    // Reserve bits for element
-                    generationInfo.addStateIndex(id, stateIndex);
-                    stateIndex += 2;
-
-                    if (isRepresentative(id)) {
-                        generationInfo.addSpareActivationIndex(id, stateIndex);
-                        ++stateIndex;
-                    }
-
-                    if (element->isSpareGate()) {
-                        generationInfo.addSpareUsageIndex(id, stateIndex);
-                        stateIndex += generationInfo.usageInfoBits();
-                    }
-                    
-                }
-                
                 if (consideredDependencies) {
                     break;
                 }
                 
+                stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
+                
                 // Consider dependencies
                 for (size_t idDependency : getDependencies()) {
                     std::shared_ptr<DFTDependency<ValueType> const> dependency = getDependency(idDependency);
@@ -134,8 +103,43 @@ namespace storm {
             
             return generationInfo;
         }
-
-
+        
+        template<typename ValueType>
+        size_t DFT<ValueType>::performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue<size_t>& visitQueue, std::set<size_t>& visited, size_t stateIndex) const {
+            while (!visitQueue.empty()) {
+                size_t id = visitQueue.front();
+                visitQueue.pop();
+                if (visited.count(id) == 1) {
+                    // Already visited
+                    continue;
+                }
+                visited.insert(id);
+                DFTElementPointer element = mElements[id];
+                
+                // Insert children
+                if (element->isGate()) {
+                    for (auto const& child : std::static_pointer_cast<DFTGate<ValueType>>(element)->children()) {
+                        visitQueue.push(child->id());
+                    }
+                }
+                
+                // Reserve bits for element
+                generationInfo.addStateIndex(id, stateIndex);
+                stateIndex += 2;
+                
+                if (isRepresentative(id)) {
+                    generationInfo.addSpareActivationIndex(id, stateIndex);
+                    ++stateIndex;
+                }
+                
+                if (element->isSpareGate()) {
+                    generationInfo.addSpareUsageIndex(id, stateIndex);
+                    stateIndex += generationInfo.usageInfoBits();
+                }
+                
+            }
+            return stateIndex;
+        }
 
         template<typename ValueType>
         std::string DFT<ValueType>::getElementsString() const {
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index 2ee1a2edf..3beacf8d9 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -127,6 +127,8 @@ namespace storm {
             
             DFTStateGenerationInfo buildStateGenerationInfo(std::vector<size_t> const& subTreeRoots, std::vector<std::vector<size_t>> const& symmetries) const;
 
+            size_t performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue<size_t>& visitQueue, std::set<size_t>& visited, size_t stateIndex) const;
+            
             size_t stateVectorSize() const {
                 return mStateVectorSize;
             }