diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index c46b9d84c..2aa557d8c 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -321,7 +321,7 @@ namespace storm { template std::vector DFT::getIndependentSubDftRoots(size_t index) const { auto elem = getElement(index); - auto ISD = elem->independentSubDft(); + auto ISD = elem->independentSubDft(false); return ISD; } @@ -373,8 +373,8 @@ namespace storm { if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) { std::cout << "Considering ids " << *it1 << ", " << *it2 << " for isomorphism." << std::endl; bool isSymmetry = false; - std::vector isubdft1 = getGate(*it1)->independentSubDft(); - std::vector isubdft2 = getGate(*it2)->independentSubDft(); + std::vector isubdft1 = getGate(*it1)->independentSubDft(false); + std::vector isubdft2 = getGate(*it2)->independentSubDft(false); if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) { continue; } diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index 5e5c3da84..e3889bf4d 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -57,16 +57,7 @@ namespace storm { dependentEvent->addIngoingDependency(dependency); } -// for (auto& restriction : mRestrictions) { -// std::set parentsOfRestrictedElements; -// for (auto& child : restriction->children()) { -// for(DFTGatePointer& parent : child->parents()) { -// parentsOfRestrictedElements.insert(parent); -// } -// } -// -// -// } + // Sort elements topologically // compute rank diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index ecb6c049c..4cf49e0b0 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -63,7 +63,7 @@ namespace storm { } template - std::vector DFTElement::independentSubDft() const { + std::vector DFTElement::independentSubDft(bool blockParents) const { //std::cout << "INDEPENDENT SUBTREE CALL " << this->id() << std::endl; std::vector res; res.push_back(this->id()); @@ -71,7 +71,7 @@ namespace storm { } template - void DFTElement::extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const { + void DFTElement::extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) 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. @@ -80,14 +80,16 @@ namespace storm { } elemsInSubtree.insert(mId); for(auto const& parent : mParents) { - - parent->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(blockParents && std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), parent->id()) != parentsOfSubRoot.end()) { + continue; + } + parent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { return; } } for(auto const& dep : mOutgoingDependencies) { - dep->extendSubDft(elemsInSubtree, parentsOfSubRoot); + dep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { return; } @@ -95,7 +97,7 @@ namespace storm { } for(auto const& restr : mRestrictions) { - restr->extendSubDft(elemsInSubtree, parentsOfSubRoot); + restr->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { return; } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 43db2c46e..dc07505bd 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -262,15 +262,15 @@ namespace storm { /** * Computes independent subtrees starting with this element (this), that is, all elements (x) which are connected to either * - one of the children of the element, - * - a propabilisistic dependency + * - 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() const; + virtual std::vector independentSubDft(bool blockParents) const; /** * Helper to the independent subtree computation * @see independentSubDft */ - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const; + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const; virtual bool isTypeEqualTo(DFTElement const& other) const { return type() == other.type(); @@ -351,8 +351,8 @@ namespace storm { } } - virtual std::vector independentSubDft() const override { - auto prelRes = DFTElement::independentSubDft(); + virtual std::vector independentSubDft(bool blockParents) 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; @@ -360,7 +360,7 @@ namespace storm { std::set unit(prelRes.begin(), prelRes.end()); std::vector pids = this->parentIds(); for(auto const& child : mChildren) { - child->extendSubDft(unit, pids); + child->extendSubDft(unit, pids, blockParents); if(unit.empty()) { // Parent in the subdft, ie it is *not* a subdft break; @@ -369,15 +369,15 @@ namespace storm { return std::vector(unit.begin(), unit.end()); } - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const override { if(elemsInSubtree.count(this->id()) > 0) return; - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } for(auto const& child : mChildren) { - child->extendSubDft(elemsInSubtree, parentsOfSubRoot); + child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; @@ -531,15 +531,15 @@ namespace storm { return storm::utility::isZero(mPassiveFailureRate); } - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const override { if(elemsInSubtree.count(this->id())) return; - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } for(auto const& incDep : mIngoingDependencies) { - incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot); + incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; @@ -683,19 +683,19 @@ namespace storm { return std::vector(unit.begin(), unit.end()); } - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const override { if(elemsInSubtree.count(this->id())) return; - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } - mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot); + mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } - mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot); + mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); } diff --git a/src/storage/dft/elements/DFTRestriction.h b/src/storage/dft/elements/DFTRestriction.h index d0482e4a7..70163a6e6 100644 --- a/src/storage/dft/elements/DFTRestriction.h +++ b/src/storage/dft/elements/DFTRestriction.h @@ -66,8 +66,8 @@ namespace storm { } } - virtual std::vector independentSubDft() const override { - auto prelRes = DFTElement::independentSubDft(); + virtual std::vector independentSubDft(bool blockParents) 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; @@ -75,7 +75,7 @@ namespace storm { std::set unit(prelRes.begin(), prelRes.end()); std::vector pids = this->parentIds(); for(auto const& child : mChildren) { - child->extendSubDft(unit, pids); + child->extendSubDft(unit, pids, blockParents); if(unit.empty()) { // Parent in the subdft, ie it is *not* a subdft break; @@ -84,15 +84,15 @@ namespace storm { return std::vector(unit.begin(), unit.end()); } - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const override { if(elemsInSubtree.count(this->id()) > 0) return; - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } for(auto const& child : mChildren) { - child->extendSubDft(elemsInSubtree, parentsOfSubRoot); + child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; @@ -183,7 +183,7 @@ namespace storm { } - bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { }