diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 29f97d77c..b05e57eda 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -1,3 +1,5 @@ +#include + #include "DFT.h" namespace storm { @@ -142,7 +144,13 @@ namespace storm { return stream.str(); } + template + bool DFT::rootOfClosedSubDFT(size_t index) const { + //boost::container::flat_set marked; + //DFTElementPointer elem = getElement(index); + + } // Explicitly instantiate the class. template class DFT; diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 2cfbf6422..ec68e1f30 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -191,7 +191,7 @@ namespace storm { std::string getStateString(DFTStatePointer const& state) const; - DFTIsomorphisms detectIsomorphicChildren() const; + bool rootOfClosedSubDFT(size_t id) const; private: bool elementIndicesCorrect() const { for(size_t i = 0; i < mElements.size(); ++i) { diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index 0c18e3be6..761975762 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -34,9 +34,30 @@ namespace storm { template void DFTElement::extendUnit(std::set& unit) const { unit.insert(mId); + } + + template + std::vector DFTElement::independentSubDft() const { + 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 { + 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(); + return; + } + elemsInSubtree.insert(mId); for(auto const& parent : mParents) { - if(unit.count(parent->id()) != 0) { - parent->extendUnit(unit); + if(elemsInSubtree.count(parent->id()) != 0) { + parent->extendUnit(elemsInSubtree); + if(elemsInSubtree.empty()) { + return; + } } } } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 7f92ebb19..b047ddbd1 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -42,11 +42,13 @@ namespace storm { virtual ~DFTElement() {} - + /** + * Returns the id + */ virtual size_t id() const { return mId; } - + virtual void setRank(size_t rank) { mRank = rank; } @@ -62,7 +64,10 @@ namespace storm { virtual bool isGate() const { return false; } - + + /** + * Returns true if the element is a BE + */ virtual bool isBasicElement() const { return false; } @@ -70,7 +75,10 @@ namespace storm { virtual bool isColdBasicElement() const { return false; } - + + /** + * Returns true if the element is a spare gate + */ virtual bool isSpareGate() const { return false; } @@ -78,7 +86,10 @@ namespace storm { virtual void setId(size_t newId) { mId = newId; } - + + /** + * Returns the name + */ virtual std::string const& name() const { return mName; } @@ -101,7 +112,15 @@ namespace storm { DFTGateVector const& parents() const { return mParents; } - + + std::vector parentIds() const { + std::vector res; + for(auto parent : parents()) { + res.push_back(parent->id()); + } + return res; + } + virtual void extendSpareModule(std::set& elementsInModule) const; virtual size_t nrChildren() const = 0; @@ -109,12 +128,33 @@ namespace storm { virtual std::string toString() const = 0; virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; - + + /** + * Computes the independent unit of this element, that is, all elements which are direct or indirect successors of an element. + */ virtual std::vector independentUnit() const = 0; - + + /** + * Helper to independent unit computation + * @see independentUnit + */ virtual void extendUnit(std::set& unit) const; + /** + * 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 + * such that there exists a path from x to a child of this does not go through this. + */ + virtual std::vector independentSubDft() const; + /** + * Helper to the independent subtree computation + * @see independentSubDft + */ + virtual void extendSubDft(std::set elemsInSubtree, std::vector const& parentsOfSubRoot) const; + void checkForSymmetricChildren() const; + }; @@ -197,13 +237,50 @@ namespace storm { for(auto const& child : mChildren) { child->extendUnit(unit); } - for(auto const& parent : this->mParents) { - if(unit.count(parent->id()) != 0) { - return {}; - } + return std::vector(unit.begin(), unit.end()); + } + + virtual void extendUnit(std::set& unit) const override { + DFTElement::extendUnit(unit); + for(auto const& child : mChildren) { + child->extendUnit(unit); + } + } + + virtual std::vector independentSubDft() const override { + auto prelRes = DFTElement::independentSubDft(); + 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(); + for(auto const& child : mChildren) { + child->extendSubDft(unit, pids); + if(unit.empty()) { + // Parent in the subdft, ie it is *not* a subdft + break; + } } return std::vector(unit.begin(), unit.end()); } + + virtual void extendSubDft(std::set elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(!elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + for(auto const& child : mChildren) { + child->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + break; + } + } + } + + virtual std::string toString() const override { std::stringstream stream; @@ -226,13 +303,7 @@ namespace storm { } return false; } - - virtual void extendUnit(std::set& unit) const override { - DFTElement::extendUnit(unit); - for(auto const& child : mChildren) { - child->extendUnit(unit); - } - } + protected: @@ -318,10 +389,11 @@ namespace storm { return storm::utility::isZero(mPassiveFailureRate); } - virtual std::vector independentUnit() const { + virtual std::vector independentUnit() const override { return {this->mId}; } + virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; };