diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index fffd33946..00e416d54 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -109,7 +109,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type handled separately."); case DFTElementType::CONSTF: case DFTElementType::CONSTS: - case DFTElementType::FDEP: + case DFTElementType::PDEP: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported."); default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known."); diff --git a/src/storage/dft/DFTElementType.h b/src/storage/dft/DFTElementType.h index 9aba9fa54..98d58df5c 100644 --- a/src/storage/dft/DFTElementType.h +++ b/src/storage/dft/DFTElementType.h @@ -4,7 +4,7 @@ namespace storm { namespace storage { - enum class DFTElementType : int {AND = 0, COUNTING = 1, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, FDEP = 10, SEQAND = 11}; + 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) { @@ -20,7 +20,7 @@ namespace storm { case DFTElementType::BE: case DFTElementType::CONSTF: case DFTElementType::CONSTS: - case DFTElementType::FDEP: + case DFTElementType::PDEP: return false; default: assert(false); diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index fb5123180..a6ee87ea5 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -51,6 +51,8 @@ namespace storm { return mId; } + virtual DFTElementType type() const = 0; + virtual void setRank(size_t rank) { mRank = rank; } @@ -114,7 +116,11 @@ namespace storm { bool hasParents() const { return !mParents.empty(); } - + + size_t nrParents() const { + return mParents.size(); + } + DFTGateVector const& parents() const { return mParents; } @@ -348,7 +354,11 @@ namespace storm { DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) : DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate) {} - + + DFTElementType type() const override { + return DFTElementType::BE; + } + virtual size_t nrChildren() const { return 0; } @@ -393,7 +403,16 @@ namespace storm { DFTConst(size_t id, std::string const& name, bool failed) : DFTElement(id, name), mFailed(failed) {} - + + DFTElementType type() const override { + if(mFailed) { + return DFTElementType::CONSTF; + } else { + return DFTElementType::CONSTS; + } + } + + bool failed() const { return mFailed; } @@ -438,15 +457,15 @@ namespace storm { mDependentEvent = dependentEvent; } - std::string nameTrigger() { + std::string nameTrigger() const { return mNameTrigger; } - std::string nameDependent() { + std::string nameDependent() const { return mNameDependent; } - ValueType probability() { + ValueType const& probability() const { return mProbability; } @@ -460,6 +479,10 @@ namespace storm { return mDependentEvent; } + DFTElementType type() const override { + return DFTElementType::PDEP; + } + virtual size_t nrChildren() const override { return 1; } @@ -519,6 +542,10 @@ namespace storm { this->childrenDontCare(state, queues); } } + + virtual DFTElementType type() const override { + return DFTElementType::AND; + } std::string typestring() const { return "AND"; @@ -555,6 +582,10 @@ namespace storm { } this->failsafe(state, queues); } + + virtual DFTElementType type() const override { + return DFTElementType::OR; + } std::string typestring() const { return "OR"; @@ -606,8 +637,12 @@ namespace storm { } //return false; } - - std::string typestring() const { + + virtual DFTElementType type() const override { + return DFTElementType::SEQAND; + } + + std::string typestring() const override { return "SEQAND"; } }; @@ -653,8 +688,12 @@ namespace storm { this->childrenDontCare(state, queues); } } + + virtual DFTElementType type() const override { + return DFTElementType::PAND; + } - std::string typestring() const { + std::string typestring() const override { return "PAND"; } }; @@ -680,8 +719,12 @@ namespace storm { void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ assert(false); } + + virtual DFTElementType type() const override { + return DFTElementType::POR; + } - std::string typestring() const { + std::string typestring() const override { return "POR"; } }; @@ -740,6 +783,10 @@ namespace storm { } } } + + virtual DFTElementType type() const override { + return DFTElementType::VOT; + } std::string typestring() const { return "VOT (" + std::to_string(mThreshold) + ")"; @@ -766,11 +813,15 @@ namespace storm { DFTGate(id, name, children) {} - std::string typestring() const { + std::string typestring() const override { return "SPARE"; } - - bool isSpareGate() const { + + virtual DFTElementType type() const override { + return DFTElementType::SPARE; + } + + bool isSpareGate() const override { return true; }