intermediate commit

Former-commit-id: 2de6f91062

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) {

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;
+                }
+            }
+            
         }
 
 

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> {