diff --git a/src/storage/dft/DFTElementType.h b/src/storage/dft/DFTElementType.h index 98d58df5c..a32745cdf 100644 --- a/src/storage/dft/DFTElementType.h +++ b/src/storage/dft/DFTElementType.h @@ -6,6 +6,7 @@ namespace storm { enum class DFTElementType : int {AND = 0, COUNTING = 1, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, PDEP = 10, SEQAND = 11}; + inline bool isGateType(DFTElementType const& tp) { switch(tp) { case DFTElementType::AND: @@ -24,9 +25,30 @@ namespace storm { return false; default: assert(false); + return false; } } + + inline bool isStaticGateType(DFTElementType const& tp) { + if(!isGateType(tp)) return false; + switch(tp) { + case DFTElementType::AND: + case DFTElementType::OR: + case DFTElementType::VOT: + return true; + case DFTElementType::POR: + case DFTElementType::SPARE: + case DFTElementType::PAND: + case DFTElementType::SEQAND: + return false; + default: + assert(false); + return false; + } + } + + } } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index d7060654f..36075d005 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -118,10 +118,20 @@ namespace storm { } } + bool hasOnlyStaticParents() const { + for(auto const& parent : mParents) { + if(!isStaticGateType(parent->type())) { + return false; + } + } + return true; + } + + bool hasParents() const { return !mParents.empty(); } - + size_t nrParents() const { return mParents.size(); } @@ -194,7 +204,9 @@ namespace storm { */ virtual void extendSubDft(std::set<size_t> elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const; - + virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const { + return type() == other.type(); + } protected: @@ -368,7 +380,7 @@ namespace storm { } return false; } - + }; @@ -442,6 +454,13 @@ namespace storm { bool isColdBasicElement() const override{ return storm::utility::isZero(mPassiveFailureRate); } + + bool isTypeEqualTo(DFTElement<ValueType> const& other) const override { + if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false; + DFTBE<ValueType> const& otherBE = static_cast<DFTBE<ValueType> const&>(other); + return (mActiveFailureRate == otherBE.mActiveFailureRate) && (mPassiveFailureRate == otherBE.mPassiveFailureRate); + } + virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override; }; @@ -483,6 +502,12 @@ namespace storm { return 0; } + bool isTypeEqualTo(DFTElement<ValueType> const& other) const override { + if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false; + DFTConst<ValueType> const& otherCNST = static_cast<DFTConst<ValueType> const&>(other); + return (mFailed == otherCNST.mFailed); + } + }; @@ -547,6 +572,13 @@ namespace storm { virtual bool isDependency() const override { return true; } + + virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const override { + if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false; + DFTDependency<ValueType> const& otherDEP= static_cast<DFTDependency<ValueType> const&>(other); + return (mProbability == otherDEP.mProbability); + } + virtual std::vector<size_t> independentUnit() const override { std::set<size_t> unit = {this->mId}; @@ -848,7 +880,12 @@ namespace storm { std::string typestring() const override{ return "VOT (" + std::to_string(mThreshold) + ")"; } - + + virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const override { + if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false; + DFTVot<ValueType> const& otherVOT = static_cast<DFTVot<ValueType> const&>(other); + return (mThreshold == otherVOT.mThreshold); + } }; template<typename ValueType> @@ -916,7 +953,12 @@ namespace storm { } } }; - + + template<typename ValueType> + bool equalType(DFTElement<ValueType> const& e1, DFTElement<ValueType> const& e2) { + return e1.isTypeEqualTo(e2); + } + } }