First version of symmetry for shared spares. Still some problems in contrast to Dortmund which had absolutely no problems with Tottenham.

Former-commit-id: c03062d4bd

examples/dft/symmetry_shared.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" and "B" "B'";
+"B" wsp "C" "D";
+"B'" wsp "C'" "D";
+"C" lambda=0.5 dorm=0;
+"D" lambda=0.5 dorm=0;
+"C'" lambda=0.5 dorm=0;

src/storage/dft/DFT.cpp

@@ -454,6 +454,98 @@ namespace storm {
             return DFTColouring<ValueType>(*this);
         }
 
+        template<typename ValueType>
+        std::map<size_t, size_t> DFT<ValueType>::findBijection(size_t index1, size_t index2, DFTColouring<ValueType> const& colouring, bool sparesAsLeaves) const {
+            STORM_LOG_TRACE("Considering ids " << index1 << ", " << index2 << " for isomorphism.");
+            bool sharedSpareMode = false;
+            std::map<size_t, size_t> bijection;
+            
+            if (isBasicElement(index1)) {
+                if (!isBasicElement(index2)) {
+                    return {};
+                }
+                if (colouring.hasSameColour(index1, index2)) {
+                    bijection[index1] = index2;
+                    return bijection;
+                } else {
+                    return {};
+                }
+            }
+            
+            assert(isGate(index1));
+            assert(isGate(index2));
+            std::vector<size_t> isubdft1 = getGate(index1)->independentSubDft(false);
+            std::vector<size_t> isubdft2 = getGate(index2)->independentSubDft(false);
+            if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) {
+                if (isubdft1.empty() && isubdft2.empty() && sparesAsLeaves) {
+                    // Check again for shared spares
+                    sharedSpareMode = true;
+                    isubdft1 = getGate(index1)->independentSubDft(false, true);
+                    isubdft2 = getGate(index2)->independentSubDft(false, true);
+                    if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) {
+                        return {};
+                    }
+                } else {
+                    return {};
+                }
+            }
+            STORM_LOG_TRACE("Checking subdfts from " << index1 << ", " << index2 << " for isomorphism.");
+            auto LHS = colouring.colourSubdft(isubdft1);
+            auto RHS = colouring.colourSubdft(isubdft2);
+            auto IsoCheck = DFTIsomorphismCheck<ValueType>(LHS, RHS, *this);
+            
+            while (IsoCheck.findNextIsomorphism()) {
+                bijection = IsoCheck.getIsomorphism();
+                if (sharedSpareMode) {
+                    bool bijectionSpareCompatible = true;
+                    for (size_t elementId : isubdft1) {
+                        if (getElement(elementId)->isSpareGate()) {
+                            std::shared_ptr<DFTSpare<ValueType>> spareLeft = std::static_pointer_cast<DFTSpare<ValueType>>(mElements[elementId]);
+                            std::shared_ptr<DFTSpare<ValueType>> spareRight = std::static_pointer_cast<DFTSpare<ValueType>>(mElements[bijection.at(elementId)]);
+                            
+                            if (spareLeft->nrChildren() != spareRight->nrChildren()) {
+                                bijectionSpareCompatible = false;
+                                break;
+                            }
+                            // Check bijection for spare children
+                            for (size_t i = 0; i < spareLeft->nrChildren(); ++i) {
+                                size_t childLeftId = spareLeft->children().at(i)->id();
+                                size_t childRightId = spareRight->children().at(i)->id();
+
+                                assert(bijection.count(childLeftId) == 0);
+                                if (childLeftId == childRightId) {
+                                    // Ignore shared child
+                                    continue;
+                                }
+                                
+                                // TODO generalize for more than one parent
+                                if (spareLeft->children().at(i)->nrParents() != 1 || spareRight->children().at(i)->nrParents() != 1) {
+                                    bijectionSpareCompatible = false;
+                                    break;
+                                }
+                                
+                                std::map<size_t, size_t> tmpBijection = findBijection(childLeftId, childRightId, colouring, false);
+                                if (!tmpBijection.empty()) {
+                                    bijection.insert(tmpBijection.begin(), tmpBijection.end());
+                                } else {
+                                    bijectionSpareCompatible = false;
+                                    break;
+                                }
+                            }
+                            if (!bijectionSpareCompatible) {
+                                break;
+                            }
+                        }
+                    }
+                    if (bijectionSpareCompatible) {
+                        return bijection;
+                    }
+                } else {
+                    return bijection;
+                }
+            } // end while
+            return {};
+        }
 
         template<typename ValueType>
         DFTIndependentSymmetries DFT<ValueType>::findSymmetries(DFTColouring<ValueType> const& colouring) const {
@@ -486,33 +578,21 @@ namespace storm {
                             std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end());
                             
                             if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) {
-                                STORM_LOG_TRACE("Considering ids " << *it1 << ", " << *it2 << " for isomorphism.");
-                                bool isSymmetry = false;
-                                std::vector<size_t> isubdft1 = getGate(*it1)->independentSubDft(false);
-                                std::vector<size_t> isubdft2 = getGate(*it2)->independentSubDft(false);
-                                if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) {
-                                    continue;
-                                }
-                                STORM_LOG_TRACE("Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism.");
-                                auto LHS = colouring.colourSubdft(isubdft1);
-                                auto RHS = colouring.colourSubdft(isubdft2);
-                                auto IsoCheck = DFTIsomorphismCheck<ValueType>(LHS, RHS, *this);
-                                isSymmetry = IsoCheck.findIsomorphism();
-                                if(isSymmetry) {
+                                std::map<size_t, size_t> bijection = findBijection(*it1, *it2, colouring, true);
+                                if (!bijection.empty()) {
                                     STORM_LOG_TRACE("Subdfts are symmetric");
                                     foundEqClassFor.insert(*it2);
                                     if(symClass.empty()) {
-                                        for(auto const& i : isubdft1) {
-                                            symClass.push_back(std::vector<size_t>({i}));
+                                        for(auto const& i : bijection) {
+                                            symClass.push_back(std::vector<size_t>({i.first}));
                                         }
                                     }
                                     auto symClassIt = symClass.begin();
-                                    for(auto const& i : isubdft1) {
-                                        symClassIt->emplace_back(IsoCheck.getIsomorphism().at(i));
+                                    for(auto const& i : bijection) {
+                                        symClassIt->emplace_back(i.second);
                                         ++symClassIt;
                                         
                                     }
-                                    
                                 }
                             }
                         }

src/storage/dft/DFT.h

@@ -238,6 +238,8 @@ namespace storm {
             std::vector<size_t> getIndependentSubDftRoots(size_t index) const;
 
             DFTColouring<ValueType> colourDFT() const;
+            
+            std::map<size_t, size_t> findBijection(size_t index1, size_t index2, DFTColouring<ValueType> const& colouring, bool sparesAsLeaves) const;
 
             DFTIndependentSymmetries findSymmetries(DFTColouring<ValueType> const& colouring) const;
 

src/storage/dft/DFTIsomorphism.h

@@ -202,6 +202,10 @@ namespace storage {
                 }
             }
         }
+        
+        bool hasSameColour(size_t index1, size_t index2) const {
+            return beColour.at(index1) == beColour.at(index2);
+        }
 
 
         BijectionCandidates<ValueType> colourSubdft(std::vector<size_t> const& subDftIndices) const {
@@ -308,13 +312,21 @@ namespace storage {
         }
 
         /**
-         * Check whether an isomorphism exists.
+         * Check whether another isomorphism exists.
          *
-         * @return true iff an isomorphism exists.
+         * @return true iff another isomorphism exists.
          */
-        bool findIsomorphism() {
-            if(!candidatesCompatible) return false;
-            constructInitialBijection();
+        bool findNextIsomorphism() {
+            if(!candidatesCompatible){
+                return false;
+            }
+            if (bijection.empty()) {
+                constructInitialBijection();
+            } else {
+                if (!findNextBijection()) {
+                    return false;
+                }
+            }
             while(!check()) {
                 // continue our search
                 if(!findNextBijection()) {
@@ -382,19 +394,31 @@ namespace storage {
 
             if(foundNext) {
                 for(auto const& colour : bleft.beCandidates) {
-                    zipVectorsIntoMap(colour.second, currentPermutations.beCandidates.find(colour.first)->second, bijection);
+                    if (colour.second.size() > 1) {
+                        assert(currentPermutations.beCandidates.find(colour.first) != currentPermutations.beCandidates.end());
+                        zipVectorsIntoMap(colour.second, currentPermutations.beCandidates.find(colour.first)->second, bijection);
+                    }
                 }
 
                 for(auto const& colour : bleft.gateCandidates) {
-                    zipVectorsIntoMap(colour.second, currentPermutations.gateCandidates.find(colour.first)->second, bijection);
+                    if (colour.second.size() > 1) {
+                        assert(currentPermutations.gateCandidates.find(colour.first) != currentPermutations.gateCandidates.end());
+                        zipVectorsIntoMap(colour.second, currentPermutations.gateCandidates.find(colour.first)->second, bijection);
+                    }
                 }
 
                 for(auto const& colour : bleft.pdepCandidates) {
-                    zipVectorsIntoMap(colour.second, currentPermutations.pdepCandidates.find(colour.first)->second, bijection);
+                    if (colour.second.size() > 1) {
+                        assert(currentPermutations.pdepCandidates.find(colour.first) != currentPermutations.pdepCandidates.end());
+                        zipVectorsIntoMap(colour.second, currentPermutations.pdepCandidates.find(colour.first)->second, bijection);
+                    }
                 }
                 
                 for(auto const& colour : bleft.restrictionCandidates) {
-                    zipVectorsIntoMap(colour.second, currentPermutations.restrictionCandidates.find(colour.first)->second, bijection);
+                    if (colour.second.size() > 1) {
+                        assert(currentPermutations.restrictionCandidates.find(colour.first) != currentPermutations.restrictionCandidates.end());
+                        zipVectorsIntoMap(colour.second, currentPermutations.restrictionCandidates.find(colour.first)->second, bijection);
+                    }
                 }
             }
 
@@ -405,7 +429,7 @@ namespace storage {
         /**
          *
          */
-        bool check() {
+        bool check() const {
             assert(bijection.size() == bleft.size());
             // We can skip BEs, as they are identified by they're homomorphic if they are in the same class
             for(auto const& indexpair : bijection) {
@@ -418,13 +442,23 @@ namespace storage {
                     if(lGate->isDynamicGate()) {
                         std::vector<size_t> childrenLeftMapped;
                         for(auto const& child : lGate->children() ) {
-                            assert(bleft.has(child->id()));
-                            childrenLeftMapped.push_back(bijection.at(child->id()));
+                            if (bleft.has(child->id())) {
+                                childrenLeftMapped.push_back(bijection.at(child->id()));
+                            } else {
+                                // Indicate shared child which is not part of the symmetry
+                                // For dynamic gates the order is important
+                                childrenLeftMapped.push_back(-1);
+                            }
                         }
                         std::vector<size_t> childrenRight;
                         for(auto const& child : rGate->children() ) {
-                            assert(bright.has(child->id()));
-                            childrenRight.push_back(child->id());
+                            if (bright.has(child->id())) {
+                                childrenRight.push_back(child->id());
+                            } else {
+                                // Indicate shared child which is not part of the symmetry
+                                // For dynamic gates the order is important
+                                childrenRight.push_back(-1);
+                            }
                         }
                         if(childrenLeftMapped != childrenRight) {
                             return false;
@@ -432,13 +466,15 @@ namespace storage {
                     } else {
                         std::set<size_t> childrenLeftMapped;
                         for(auto const& child : lGate->children() ) {
-                            assert(bleft.has(child->id()));
-                            childrenLeftMapped.insert(bijection.at(child->id()));
+                            if (bleft.has(child->id())) {
+                                childrenLeftMapped.insert(bijection.at(child->id()));
+                            }
                         }
                         std::set<size_t> childrenRight;
                         for(auto const& child : rGate->children() ) {
-                            assert(bright.has(child->id()));
-                            childrenRight.insert(child->id());
+                            if (bright.has(child->id())) {
+                                childrenRight.insert(child->id());
+                            }
                         }
                         if(childrenLeftMapped != childrenRight) {
                             return false;
@@ -459,16 +495,26 @@ namespace storage {
                 } else if(dft.isRestriction(indexpair.first)) {
                     assert(dft.isRestriction(indexpair.second));
                     auto const& lRestr = dft.getRestriction(indexpair.first);
-                    std::set<size_t> childrenLeftMapped;
+                    std::vector<size_t> childrenLeftMapped;
                     for(auto const& child : lRestr->children() ) {
-                        assert(bleft.has(child->id()));
-                        childrenLeftMapped.insert(bijection.at(child->id()));
+                        if (bleft.has(child->id())) {
+                            childrenLeftMapped.push_back(bijection.at(child->id()));
+                        } else {
+                            // Indicate shared child which is not part of the symmetry
+                            // For dynamic gates the order is important
+                            childrenLeftMapped.push_back(-1);
+                        }
                     }
                     auto const& rRestr = dft.getRestriction(indexpair.second);
-                    std::set<size_t> childrenRight;
+                    std::vector<size_t> childrenRight;
                     for(auto const& child : rRestr->children() ) {
-                        assert(bright.has(child->id()));
-                        childrenRight.insert(child->id());
+                        if (bright.has(child->id())) {
+                            childrenRight.push_back(child->id());
+                        } else {
+                            // Indicate shared child which is not part of the symmetry
+                            // For dynamic gates the order is important
+                            childrenRight.push_back(-1);
+                        }
                     }
                     if(childrenLeftMapped != childrenRight) {
                         return false;
@@ -487,50 +533,51 @@ namespace storage {
         /**
          * Returns true if the colours are compatible.
          */
-        void checkCompatibility() {
+        bool checkCompatibility() {
             if(bleft.gateCandidates.size() != bright.gateCandidates.size()) {
                 candidatesCompatible = false;
-                return;
+                return false;
             }
             if(bleft.beCandidates.size() != bright.beCandidates.size()) {
                 candidatesCompatible = false;
-                return;
+                return false;
             }
             if(bleft.beCandidates.size() != bright.beCandidates.size()) {
                 candidatesCompatible = false;
-                return;
+                return false;
             }
             if(bleft.restrictionCandidates.size() != bright.restrictionCandidates.size()) {
                 candidatesCompatible = false;
-                return;
+                return false;
             }
             
             for (auto const &gc : bleft.gateCandidates) {
                 if (bright.gateCandidates.count(gc.first) == 0) {
                     candidatesCompatible = false;
-                    return;
+                    return false;
                 }
             }
             for(auto const& bc : bleft.beCandidates) {
                 if(bright.beCandidates.count(bc.first) == 0) {
                     candidatesCompatible = false;
-                    return;
+                    return false;
                 }
             }
                
             for(auto const& dc : bleft.pdepCandidates) {
                 if(bright.pdepCandidates.count(dc.first) == 0) {
                     candidatesCompatible = false;
-                    return;
+                    return false;
                 }
             }
             
             for(auto const& dc : bleft.restrictionCandidates) {
                 if(bright.restrictionCandidates.count(dc.first) == 0) {
                     candidatesCompatible = false;
-                    return;
+                    return false;
                 }
             }
+            return true;
         }
 
         /**

src/storage/dft/elements/DFTBE.h

@@ -71,15 +71,15 @@ namespace storm {
                 return storm::utility::isZero(mPassiveFailureRate);
             }
             
-            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
                  if(elemsInSubtree.count(this->id())) return;
-                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                 if(elemsInSubtree.empty()) {
                     // Parent in the subdft, ie it is *not* a subdft
                     return;
                 }
                 for(auto const& incDep : mIngoingDependencies) {
-                    incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                    incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                     if(elemsInSubtree.empty()) {
                         // Parent in the subdft, ie it is *not* a subdft
                         return;

src/storage/dft/elements/DFTDependency.h

@@ -83,20 +83,19 @@ namespace storm {
                 return std::vector<size_t>(unit.begin(), unit.end());
             }
 
-            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
-                 if(elemsInSubtree.count(this->id())) return;
-                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
+                if(elemsInSubtree.count(this->id())) return;
+                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                 if(elemsInSubtree.empty()) {
                     // Parent in the subdft, ie it is *not* a subdft
                     return;
                 }
-                mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                 if(elemsInSubtree.empty()) {
                     // Parent in the subdft, ie it is *not* a subdft
                     return;
                 }
-                mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
-                
+                mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                 
             }
             

src/storage/dft/elements/DFTElement.cpp

@@ -68,14 +68,14 @@ namespace storm {
         }
 
         template<typename ValueType>
-        std::vector<size_t> DFTElement<ValueType>::independentSubDft(bool blockParents) const {
+        std::vector<size_t> DFTElement<ValueType>::independentSubDft(bool blockParents, bool sparesAsLeaves) const {
             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 {
+        void DFTElement<ValueType>::extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) 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.
@@ -87,13 +87,13 @@ namespace storm {
                 if(blockParents && std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), parent->id()) != parentsOfSubRoot.end()) {
                     continue;
                 }
-                parent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                parent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                 if(elemsInSubtree.empty()) {
                     return;
                 }
             }
             for(auto const& dep : mOutgoingDependencies) {
-                dep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                dep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                 if(elemsInSubtree.empty()) {
                     return;
                 }
@@ -101,7 +101,7 @@ namespace storm {
             }
             
             for(auto const& restr : mRestrictions) {
-                restr->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                restr->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                 if(elemsInSubtree.empty()) {
                     return;
                 }

src/storage/dft/elements/DFTElement.h

@@ -286,12 +286,12 @@ namespace storm {
              *  - a probabilistic dependency
              *  such that there exists a  path from x to a child of this does not go through this.
              */
-            virtual std::vector<size_t> independentSubDft(bool blockParents) const;
+            virtual std::vector<size_t> independentSubDft(bool blockParents, bool sparesAsLeaves = false) const;
             /**
              * Helper to the independent subtree computation
              * @see independentSubDft
              */
-            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const;
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const;
 
             virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const {
                 return type() == other.type();

src/storage/dft/elements/DFTGate.h

@@ -73,7 +73,7 @@ namespace storm {
                 }
             }
 
-            virtual std::vector<size_t> independentSubDft(bool blockParents) const override {
+            virtual std::vector<size_t> independentSubDft(bool blockParents, bool sparesAsLeaves = false) const override {
                 auto prelRes = DFTElement<ValueType>::independentSubDft(blockParents);
                 if(prelRes.empty()) {
                     // No elements (especially not this->id) in the prelimanry result, so we know already that it is not a subdft.
@@ -82,7 +82,7 @@ namespace storm {
                 std::set<size_t> unit(prelRes.begin(), prelRes.end());
                 std::vector<size_t> pids = this->parentIds();
                 for(auto const& child : mChildren) {
-                    child->extendSubDft(unit, pids, blockParents);
+                    child->extendSubDft(unit, pids, blockParents, sparesAsLeaves);
                     if(unit.empty()) {
                         // Parent in the subdft, ie it is *not* a subdft
                         break;
@@ -91,15 +91,15 @@ namespace storm {
                 return std::vector<size_t>(unit.begin(), unit.end());
             }
 
-            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
                 if(elemsInSubtree.count(this->id()) > 0) return;
-                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                 if(elemsInSubtree.empty()) {
                     // Parent in the subdft, ie it is *not* a subdft
                     return;
                 }
                 for(auto const& child : mChildren) {
-                    child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                    child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                     if(elemsInSubtree.empty()) {
                         // Parent in the subdft, ie it is *not* a subdft
                         return;

src/storage/dft/elements/DFTRestriction.h

@@ -69,7 +69,7 @@ namespace storm {
                 }
             }
 
-            virtual std::vector<size_t> independentSubDft(bool blockParents) const override {
+            virtual std::vector<size_t> independentSubDft(bool blockParents, bool sparesAsLeaves) const override {
                 auto prelRes = DFTElement<ValueType>::independentSubDft(blockParents);
                 if(prelRes.empty()) {
                     // No elements (especially not this->id) in the prelimanry result, so we know already that it is not a subdft.
@@ -78,7 +78,7 @@ namespace storm {
                 std::set<size_t> unit(prelRes.begin(), prelRes.end());
                 std::vector<size_t> pids = this->parentIds();
                 for(auto const& child : mChildren) {
-                    child->extendSubDft(unit, pids, blockParents);
+                    child->extendSubDft(unit, pids, blockParents, sparesAsLeaves);
                     if(unit.empty()) {
                         // Parent in the subdft, ie it is *not* a subdft
                         break;
@@ -87,15 +87,15 @@ namespace storm {
                 return std::vector<size_t>(unit.begin(), unit.end());
             }
 
-            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
                 if(elemsInSubtree.count(this->id()) > 0) return;
-                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                 if(elemsInSubtree.empty()) {
                     // Parent in the subdft, ie it is *not* a subdft
                     return;
                 }
                 for(auto const& child : mChildren) {
-                    child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                    child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                     if(elemsInSubtree.empty()) {
                         // Parent in the subdft, ie it is *not* a subdft
                         return;

src/storage/dft/elements/DFTSpare.h

@@ -64,6 +64,45 @@ namespace storm {
                     }
                 }
             }
+            
+            std::vector<size_t> independentSubDft(bool blockParents, bool sparesAsLeaves = false) const override {
+                auto prelRes = DFTElement<ValueType>::independentSubDft(blockParents);
+                if(prelRes.empty()) {
+                    // No elements (especially not this->id) in the prelimanry result, so we know already that it is not a subdft.
+                    return prelRes;
+                }
+                std::set<size_t> unit(prelRes.begin(), prelRes.end());
+                std::vector<size_t> pids = this->parentIds();
+                if (!sparesAsLeaves) {
+                    for(auto const& child : this->mChildren) {
+                        child->extendSubDft(unit, pids, blockParents, sparesAsLeaves);
+                        if(unit.empty()) {
+                            // Parent in the subdft, ie it is *not* a subdft
+                            break;
+                        }
+                    }
+                }
+                return std::vector<size_t>(unit.begin(), unit.end());
+            }
+            
+            void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
+                if(elemsInSubtree.count(this->id()) > 0) return;
+                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
+                if(elemsInSubtree.empty()) {
+                    // Parent in the subdft, ie it is *not* a subdft
+                    return;
+                }
+                if (!sparesAsLeaves) {
+                    for(auto const& child : this->mChildren) {
+                        child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
+                        if(elemsInSubtree.empty()) {
+                            // Parent in the subdft, ie it is *not* a subdft
+                            return;
+                        }
+                    }
+                }
+            }
+
 
         };
     }