From a2a3a734a605e74b00eab861261aa15e7e0756a1 Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 11 Mar 2016 00:04:19 +0100 Subject: [PATCH] First version of symmetry for shared spares. Still some problems in contrast to Dortmund which had absolutely no problems with Tottenham. Former-commit-id: c03062d4bd4b01f949cfa5c0660d5c4906a0f9d5 --- examples/dft/symmetry_shared.dft | 7 ++ src/storage/dft/DFT.cpp | 116 ++++++++++++++++++---- src/storage/dft/DFT.h | 2 + src/storage/dft/DFTIsomorphism.h | 113 +++++++++++++++------ src/storage/dft/elements/DFTBE.h | 6 +- src/storage/dft/elements/DFTDependency.h | 11 +- src/storage/dft/elements/DFTElement.cpp | 10 +- src/storage/dft/elements/DFTElement.h | 4 +- src/storage/dft/elements/DFTGate.h | 10 +- src/storage/dft/elements/DFTRestriction.h | 10 +- src/storage/dft/elements/DFTSpare.h | 39 ++++++++ 11 files changed, 251 insertions(+), 77 deletions(-) create mode 100644 examples/dft/symmetry_shared.dft diff --git a/examples/dft/symmetry_shared.dft b/examples/dft/symmetry_shared.dft new file mode 100644 index 000000000..73ebed519 --- /dev/null +++ b/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; diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 650712ebd..e9b4c659e 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -454,6 +454,98 @@ namespace storm { return DFTColouring(*this); } + template + std::map DFT::findBijection(size_t index1, size_t index2, DFTColouring const& colouring, bool sparesAsLeaves) const { + STORM_LOG_TRACE("Considering ids " << index1 << ", " << index2 << " for isomorphism."); + bool sharedSpareMode = false; + std::map 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 isubdft1 = getGate(index1)->independentSubDft(false); + std::vector 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(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> spareLeft = std::static_pointer_cast>(mElements[elementId]); + std::shared_ptr> spareRight = std::static_pointer_cast>(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 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 DFTIndependentSymmetries DFT::findSymmetries(DFTColouring 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 isubdft1 = getGate(*it1)->independentSubDft(false); - std::vector 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(LHS, RHS, *this); - isSymmetry = IsoCheck.findIsomorphism(); - if(isSymmetry) { + std::map 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({i})); + for(auto const& i : bijection) { + symClass.push_back(std::vector({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; } - } } } diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 64805ade4..f28d244f0 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -238,6 +238,8 @@ namespace storm { std::vector getIndependentSubDftRoots(size_t index) const; DFTColouring colourDFT() const; + + std::map findBijection(size_t index1, size_t index2, DFTColouring const& colouring, bool sparesAsLeaves) const; DFTIndependentSymmetries findSymmetries(DFTColouring const& colouring) const; diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h index b1f845b9f..d94640d9c 100644 --- a/src/storage/dft/DFTIsomorphism.h +++ b/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 colourSubdft(std::vector 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 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 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 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 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 childrenLeftMapped; + std::vector 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 childrenRight; + std::vector 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; } /** diff --git a/src/storage/dft/elements/DFTBE.h b/src/storage/dft/elements/DFTBE.h index a9c5b030d..58e580262 100644 --- a/src/storage/dft/elements/DFTBE.h +++ b/src/storage/dft/elements/DFTBE.h @@ -71,15 +71,15 @@ namespace storm { return storm::utility::isZero(mPassiveFailureRate); } - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const override { + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { if(elemsInSubtree.count(this->id())) return; - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); + DFTElement::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; diff --git a/src/storage/dft/elements/DFTDependency.h b/src/storage/dft/elements/DFTDependency.h index c7f3f6bfd..44a5ab9df 100644 --- a/src/storage/dft/elements/DFTDependency.h +++ b/src/storage/dft/elements/DFTDependency.h @@ -83,20 +83,19 @@ namespace storm { return std::vector(unit.begin(), unit.end()); } - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const override { - if(elemsInSubtree.count(this->id())) return; - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { + if(elemsInSubtree.count(this->id())) return; + DFTElement::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); } diff --git a/src/storage/dft/elements/DFTElement.cpp b/src/storage/dft/elements/DFTElement.cpp index 0ee8a3cd2..803199508 100644 --- a/src/storage/dft/elements/DFTElement.cpp +++ b/src/storage/dft/elements/DFTElement.cpp @@ -68,14 +68,14 @@ namespace storm { } template - std::vector DFTElement::independentSubDft(bool blockParents) const { + std::vector DFTElement::independentSubDft(bool blockParents, bool sparesAsLeaves) const { std::vector res; res.push_back(this->id()); return res; } template - void DFTElement::extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const { + void DFTElement::extendSubDft(std::set& elemsInSubtree, std::vector 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; } diff --git a/src/storage/dft/elements/DFTElement.h b/src/storage/dft/elements/DFTElement.h index 2b3b05c98..8a8a35d28 100644 --- a/src/storage/dft/elements/DFTElement.h +++ b/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 independentSubDft(bool blockParents) const; + virtual std::vector independentSubDft(bool blockParents, bool sparesAsLeaves = false) const; /** * Helper to the independent subtree computation * @see independentSubDft */ - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const; + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const; virtual bool isTypeEqualTo(DFTElement const& other) const { return type() == other.type(); diff --git a/src/storage/dft/elements/DFTGate.h b/src/storage/dft/elements/DFTGate.h index d82906895..67fa0f70a 100644 --- a/src/storage/dft/elements/DFTGate.h +++ b/src/storage/dft/elements/DFTGate.h @@ -73,7 +73,7 @@ namespace storm { } } - virtual std::vector independentSubDft(bool blockParents) const override { + virtual std::vector independentSubDft(bool blockParents, bool sparesAsLeaves = false) const override { auto prelRes = DFTElement::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 unit(prelRes.begin(), prelRes.end()); std::vector 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(unit.begin(), unit.end()); } - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const override { + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { if(elemsInSubtree.count(this->id()) > 0) return; - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); + DFTElement::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; diff --git a/src/storage/dft/elements/DFTRestriction.h b/src/storage/dft/elements/DFTRestriction.h index dc2e6116e..25441b5b1 100644 --- a/src/storage/dft/elements/DFTRestriction.h +++ b/src/storage/dft/elements/DFTRestriction.h @@ -69,7 +69,7 @@ namespace storm { } } - virtual std::vector independentSubDft(bool blockParents) const override { + virtual std::vector independentSubDft(bool blockParents, bool sparesAsLeaves) const override { auto prelRes = DFTElement::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 unit(prelRes.begin(), prelRes.end()); std::vector 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(unit.begin(), unit.end()); } - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const override { + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { if(elemsInSubtree.count(this->id()) > 0) return; - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); + DFTElement::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; diff --git a/src/storage/dft/elements/DFTSpare.h b/src/storage/dft/elements/DFTSpare.h index dd3689311..81017ff19 100644 --- a/src/storage/dft/elements/DFTSpare.h +++ b/src/storage/dft/elements/DFTSpare.h @@ -64,6 +64,45 @@ namespace storm { } } } + + std::vector independentSubDft(bool blockParents, bool sparesAsLeaves = false) const override { + auto prelRes = DFTElement::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 unit(prelRes.begin(), prelRes.end()); + std::vector 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(unit.begin(), unit.end()); + } + + void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { + if(elemsInSubtree.count(this->id()) > 0) return; + DFTElement::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; + } + } + } + } + }; }