From fd2f83fe6de4189c3206f970f40eadaac79c16c1 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Sun, 12 Mar 2017 20:29:39 +0100
Subject: [PATCH] Consider ingoing dependencies for symmetry

---
 src/storm-dft/storage/dft/DFT.cpp | 30 +++++++++++++++++++-----------
 src/storm-dft/storage/dft/DFT.h   |  2 +-
 2 files changed, 20 insertions(+), 12 deletions(-)

diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp
index a5f2f6444..b21338c74 100644
--- a/src/storm-dft/storage/dft/DFT.cpp
+++ b/src/storm-dft/storage/dft/DFT.cpp
@@ -682,16 +682,14 @@ namespace storm {
                     continue;
                 }
 
-                std::pair<std::vector<size_t>, std::vector<size_t>> influencedElem1Ids = getSortedParentAndOutDepIds(*it1);
+                std::tuple<std::vector<size_t>, std::vector<size_t>, std::vector<size_t>> influencedElem1Ids = getSortedParentAndDependencyIds(*it1);
                 auto it2 = it1;
                 for(++it2; it2 != candidates.cend(); ++it2) {
                     if(!getElement(*it2)->hasOnlyStaticParents()) {
                         continue;
                     }
-                    std::vector<size_t> sortedParent2Ids = getElement(*it2)->parentIds();
-                    std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end());
 
-                    if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) {
+                    if(influencedElem1Ids == getSortedParentAndDependencyIds(*it2)) {
                         std::map<size_t, size_t> bijection = findBijection(*it1, *it2, colouring, true);
                         if (!bijection.empty()) {
                             STORM_LOG_TRACE("Subdfts are symmetric");
@@ -748,15 +746,25 @@ namespace storm {
     
 
         template<typename ValueType>
-        std::pair<std::vector<size_t>, std::vector<size_t>> DFT<ValueType>::getSortedParentAndOutDepIds(size_t index) const {
-            std::pair<std::vector<size_t>, std::vector<size_t>> res;
-            res.first = getElement(index)->parentIds();
-            std::sort(res.first.begin(), res.first.end());
+        std::tuple<std::vector<size_t>, std::vector<size_t>, std::vector<size_t>> DFT<ValueType>::getSortedParentAndDependencyIds(size_t index) const {
+            // Parents
+            std::vector<size_t> parents = getElement(index)->parentIds();
+            std::sort(parents.begin(), parents.end());
+            // Ingoing dependencies
+            std::vector<size_t> ingoingDeps;
+            if (isBasicElement(index)) {
+                for(auto const& dep : getBasicElement(index)->ingoingDependencies()) {
+                    ingoingDeps.push_back(dep->id());
+                }
+                std::sort(ingoingDeps.begin(), ingoingDeps.end());
+            }
+            // Outgoing dependencies
+            std::vector<size_t> outgoingDeps;
             for(auto const& dep : getElement(index)->outgoingDependencies()) {
-                res.second.push_back(dep->id());
+                outgoingDeps.push_back(dep->id());
             }
-            std::sort(res.second.begin(), res.second.end());
-            return res;
+            std::sort(outgoingDeps.begin(), outgoingDeps.end());
+            return std::make_tuple(parents, ingoingDeps, outgoingDeps);
         }
         
         // Explicitly instantiate the class.
diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h
index 815bb0df5..304018d97 100644
--- a/src/storm-dft/storage/dft/DFT.h
+++ b/src/storm-dft/storage/dft/DFT.h
@@ -276,7 +276,7 @@ namespace storm {
             }
 
         private:
-            std::pair<std::vector<size_t>, std::vector<size_t>> getSortedParentAndOutDepIds(size_t index) const;
+            std::tuple<std::vector<size_t>, std::vector<size_t>, std::vector<size_t>> getSortedParentAndDependencyIds(size_t index) const;
             
             bool elementIndicesCorrect() const {
                 for(size_t i = 0; i < mElements.size(); ++i) {