From 91970cea72d118db128c79dc89669c89ea2c3216 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 24 Feb 2016 15:28:58 +0100
Subject: [PATCH] intermediate commit

Former-commit-id: 2de6f9106211db3f5f04ac76cf101c9142a33a65
---
 src/storage/dft/DFT.h           |  2 +-
 src/storage/dft/DFTElements.cpp | 11 +++++++---
 src/storage/dft/DFTElements.h   | 37 ++++++++++++++++++++++++++++++---
 3 files changed, 43 insertions(+), 7 deletions(-)

diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index 1f3e8cceb..f0e08b31a 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -41,7 +41,7 @@ namespace storm {
             std::map<size_t, size_t> mSpareUsageIndex; // id spare -> index first bit in state
             std::map<size_t, size_t> mSpareActivationIndex; // id spare representative -> index in state
             std::vector<size_t> mIdToStateIndex; // id -> index first bit in state
-            
+            std::map<size_t, size_t> mRestrictedItems;
         public:
             
             DFTStateGenerationInfo(size_t nrElements) : mUsageInfoBits(nrElements > 1 ? storm::utility::math::uint64_log2(nrElements-1) + 1 : 1), mIdToStateIndex(nrElements) {
diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp
index 7bb8c2cf5..81c78ccc6 100644
--- a/src/storage/dft/DFTElements.cpp
+++ b/src/storage/dft/DFTElements.cpp
@@ -24,9 +24,6 @@ namespace storm {
                 }
             }
             
-            
-        
-
             state.setDontCare(mId);
             return true;
         }
@@ -85,6 +82,14 @@ namespace storm {
                 }
 
             }
+            
+            for(auto const& restr : mRestrictions) {
+                restr->extendSubDft(elemsInSubtree, parentsOfSubRoot);
+                if(elemsInSubtree.empty()) {
+                    return;
+                }
+            }
+            
         }
 
 
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index bb4be80a7..00688f36e 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -200,6 +200,40 @@ namespace storm {
                 return mOutgoingDependencies.size();
             }
             
+            std::set<DFTElement<ValueType>> restrictedItems() const {
+                std::set<DFTElement<ValueType>> result;
+                for(auto const& restr : mRestrictions) {
+                    bool foundThis = false;
+                    for(auto const& child : restr->children()) {
+                        if(!foundThis) {
+                            if(child->id() == mId) {
+                                foundThis = true;
+                            }
+                        } else if(result.count(child) == 0) {
+                            result.insert(child);
+                        }
+                    }
+                }
+            }
+            
+            std::set<DFTElement<ValueType>> restrictedItemsTC() const {
+                std::set<DFTElement<ValueType>> result;
+                for(auto const& restr : mRestrictions) {
+                    bool foundThis = false;
+                    for(auto const& child : restr->children()) {
+                        if(!foundThis) {
+                            if(child->id() == mId) {
+                                foundThis = true;
+                            }
+                        } else if(result.count(child) == 0) {
+                            result.insert(child);
+                            std::set<DFTElement<ValueType>> tmpRes = child->restrictedItemsTC();
+                            result.insert(tmpRes.begin(), tmpRes.end());
+                        }
+                    }
+                }
+            }
+            
             DFTDependencyVector const& outgoingDependencies() const {
                 return mOutgoingDependencies;
             }
@@ -784,9 +818,6 @@ namespace storm {
             return os << gate.toString();
         }
 
-
-
-
         template<typename ValueType>
         class DFTPand : public DFTGate<ValueType> {