diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index e06661988..551c7ad2a 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -37,7 +37,6 @@ namespace storm { mUsageIndex.insert(std::make_pair(elem->id(), stateIndex)); stateIndex += mUsageInfoBits; - } } @@ -68,6 +67,8 @@ namespace storm { os << std::endl; } } + + void DFT::printInfo(std::ostream& os) const { os << "Top level index: " << mTopLevelIndex << std::endl << "Nr BEs" << mNrOfBEs << std::endl; diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index b96ceafb4..699fe47e5 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -26,6 +26,19 @@ namespace storm { } } + void DFTElement::extendUnit(std::set& unit) const { + unit.insert(mId); + for(auto const& parent : mParents) { + if(unit.count(parent->id()) != 0) { + parent->extendUnit(unit); + } + } + } + + void DFTElement::checkForSymmetricChildren() const { + + } + template<> bool DFTBE::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { if(DFTElement::checkDontCareAnymore(state, queues)) { @@ -34,5 +47,6 @@ namespace storm { } return false; } + } } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 9d3338022..12da6a4bf 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -99,6 +99,10 @@ namespace storm { virtual void print(std::ostream& = std::cout) const = 0; virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; + + virtual std::vector independentUnit() const = 0; + + virtual void extendUnit(std::set& unit) const; }; @@ -166,6 +170,21 @@ namespace storm { } } + virtual std::vector independentUnit() const { + std::set unit = {mId}; + for(auto const& child : mChildren) { + child->extendUnit(unit); + } + for(auto const& parent : mParents) { + if(unit.count(parent->id()) != 0) { + return {}; + } + } + return std::vector(unit.begin(), unit.end()); + } + + + virtual void print(std::ostream& os = std::cout) const { os << "{" << name() << "} " << typestring() << "( "; std::vector>::const_iterator it = mChildren.begin(); @@ -185,7 +204,16 @@ namespace storm { } return false; } + + virtual void extendUnit(std::set& unit) const { + DFTElement::extendUnit(unit); + for(auto const& child : mChildren) { + child->extendUnit(unit); + } + } + protected: + void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { for(std::shared_ptr parent : mParents) { if(state.isOperational(parent->id())) { @@ -269,7 +297,9 @@ namespace storm { return mPassiveFailureRate == 0; } - + virtual std::vector independentUnit() const { + return {mId}; + } virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; }; diff --git a/src/storage/dft/DFTUnit.h b/src/storage/dft/DFTUnit.h new file mode 100644 index 000000000..18319b70c --- /dev/null +++ b/src/storage/dft/DFTUnit.h @@ -0,0 +1,22 @@ +#ifndef DFTUNIT_H +#define DFTUNIT_H + +namespace storm { + namespace storage { + class DFT; + + class DFTUnit { + private: + DFT const& mDft; + BitVector mMembers; + + + public: + DFTUnit(DFT const& dft, BitVector const& members); + }; + } +} + + +#endif /* DFTUNIT_H */ + diff --git a/src/storage/dft/SymmetricUnits.h b/src/storage/dft/SymmetricUnits.h new file mode 100644 index 000000000..3959593a1 --- /dev/null +++ b/src/storage/dft/SymmetricUnits.h @@ -0,0 +1,7 @@ +#ifndef SYMMETRICUNITS_H +#define SYMMETRICUNITS_H + + + +#endif /* SYMMETRICUNITS_H */ +