diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index c7fc1d960..d59ec8f41 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -46,14 +46,20 @@ namespace storm { template std::vector DFTElement::independentSubDft() const { + std::cout << "INDEPENDENT SUBTREE CALL " << this->id() << std::endl; std::vector res; res.push_back(this->id()); - // Extend for pdeps. return res; } template - void DFTElement::extendSubDft(std::set elemsInSubtree, std::vector const& parentsOfSubRoot) const { + void DFTElement::extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const { + if(elemsInSubtree.count(this->id()) > 0) return; + std::cout << "ID " << this->id() << "PREL elems "; + for(auto const& i : elemsInSubtree) { + std::cout << i << " "; + } + std::cout << "in subtree." << std::endl; if(std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) { // This is a parent of the suspected root, thus it is not a subdft. elemsInSubtree.clear(); @@ -61,13 +67,19 @@ namespace storm { } elemsInSubtree.insert(mId); for(auto const& parent : mParents) { - if(elemsInSubtree.count(parent->id()) != 0) { - parent->extendUnit(elemsInSubtree); - if(elemsInSubtree.empty()) { - return; - } + + parent->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + return; } } + for(auto const& dep : mOutgoingDependencies) { + dep->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + return; + } + + } } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index d69b73f3b..81b8ce303 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -202,7 +202,7 @@ namespace storm { * 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) const; virtual bool isTypeEqualTo(DFTElement const& other) const { return type() == other.type(); @@ -291,6 +291,11 @@ namespace storm { std::vector pids = this->parentIds(); for(auto const& child : mChildren) { child->extendSubDft(unit, pids); + std::cout << "int sub "; + for(auto const& i : unit) { + std::cout << i << " "; + } + std::cout << std::endl; if(unit.empty()) { // Parent in the subdft, ie it is *not* a subdft break; @@ -299,9 +304,10 @@ 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) const override { + if(elemsInSubtree.count(this->id()) > 0) return; DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); - if(!elemsInSubtree.empty()) { + if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } @@ -309,7 +315,7 @@ namespace storm { child->extendSubDft(elemsInSubtree, parentsOfSubRoot); if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft - break; + return; } } } @@ -437,7 +443,7 @@ namespace storm { return mIngoingDependencies.size(); } - DFTDependencyVector const& getIngoingDependencies() const { + DFTDependencyVector const& ingoingDependencies() const { return mIngoingDependencies; } @@ -455,6 +461,22 @@ namespace storm { return storm::utility::isZero(mPassiveFailureRate); } + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + if(elemsInSubtree.count(this->id())) return; + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + for(auto const& incDep : mIngoingDependencies) { + incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + } + } + bool isTypeEqualTo(DFTElement const& other) const override { if(!DFTElement::isTypeEqualTo(other)) return false; DFTBE const& otherBE = static_cast const&>(other); @@ -502,6 +524,8 @@ namespace storm { return 0; } + + bool isTypeEqualTo(DFTElement const& other) const override { if(!DFTElement::isTypeEqualTo(other)) return false; DFTConst const& otherCNST = static_cast const&>(other); @@ -589,6 +613,23 @@ namespace storm { return std::vector(unit.begin(), unit.end()); } + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + if(elemsInSubtree.count(this->id())) return; + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot); + + + } + virtual std::string toString() const override { std::stringstream stream; bool fdep = storm::utility::isOne(mProbability);