From 10c29d936bf7da08a2a161b3a68ad3d4862bed97 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 3 Apr 2019 23:17:43 +0200 Subject: [PATCH] Refactoring DFT elements --- src/storm-dft/builder/DFTBuilder.cpp | 10 +- src/storm-dft/storage/dft/DFT.cpp | 1 + src/storm-dft/storage/dft/elements/BEConst.h | 3 +- .../storage/dft/elements/BEExponential.h | 2 +- src/storm-dft/storage/dft/elements/DFTAnd.h | 45 +++--- src/storm-dft/storage/dft/elements/DFTBE.h | 16 +- .../storage/dft/elements/DFTDependency.h | 147 ++++++++++++------ src/storm-dft/storage/dft/elements/DFTGate.h | 4 +- src/storm-dft/storage/dft/elements/DFTOr.h | 46 +++--- src/storm-dft/storage/dft/elements/DFTPand.h | 77 +++++---- src/storm-dft/storage/dft/elements/DFTPor.h | 81 ++++++---- src/storm-dft/storage/dft/elements/DFTVot.h | 92 ++++++----- 12 files changed, 330 insertions(+), 194 deletions(-) diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index 56fda6401..3c856407b 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -74,12 +74,10 @@ namespace storm { childElement->addOutgoingDependency(elem.first); } } - if (binaryDependencies) { - STORM_LOG_ASSERT(dependencies.size() == 1, "Dependency '" << elem.first->name() << "' should only have one dependent element."); - } - elem.first->setDependentEvents(dependencies); - for (auto& dependency : dependencies) { - dependency->addIngoingDependency(elem.first); + STORM_LOG_ASSERT(!binaryDependencies || dependencies.size() == 1, "Dependency '" << elem.first->name() << "' should only have one dependent element."); + for (auto& be : dependencies) { + elem.first->addDependentEvent(be); + be->addIngoingDependency(elem.first); } } diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index c66af8550..a9ecb8a5a 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -621,6 +621,7 @@ namespace storm { } } } + // TODO check VOT gates return wellformed; } diff --git a/src/storm-dft/storage/dft/elements/BEConst.h b/src/storm-dft/storage/dft/elements/BEConst.h index 22cb13b9a..2cbf9fd38 100644 --- a/src/storm-dft/storage/dft/elements/BEConst.h +++ b/src/storm-dft/storage/dft/elements/BEConst.h @@ -7,6 +7,7 @@ namespace storm { /*! * BE which is either constant failed or constant failsafe. + * The BE is either always failed (from the beginning) or can never fail (failsafe). */ template class BEConst : public DFTBE { @@ -38,7 +39,7 @@ namespace storm { return this->failed(); } - bool isTypeEqualTo(DFTElement const& other) const override { + bool isTypeEqualTo(DFTElement const& other) const override { if (!DFTElement::isTypeEqualTo(other)) { return false; } diff --git a/src/storm-dft/storage/dft/elements/BEExponential.h b/src/storm-dft/storage/dft/elements/BEExponential.h index 3275aac15..8347f3179 100644 --- a/src/storm-dft/storage/dft/elements/BEExponential.h +++ b/src/storm-dft/storage/dft/elements/BEExponential.h @@ -78,7 +78,7 @@ namespace storm { return storm::utility::isZero(this->passiveFailureRate()); } - bool isTypeEqualTo(DFTElement const& other) const override { + bool isTypeEqualTo(DFTElement const& other) const override { if (!DFTElement::isTypeEqualTo(other)) { return false; } diff --git a/src/storm-dft/storage/dft/elements/DFTAnd.h b/src/storm-dft/storage/dft/elements/DFTAnd.h index c57e54c3b..aab72d436 100644 --- a/src/storm-dft/storage/dft/elements/DFTAnd.h +++ b/src/storm-dft/storage/dft/elements/DFTAnd.h @@ -1,44 +1,53 @@ -#pragma once +#pragma once + #include "DFTGate.h" namespace storm { namespace storage { + + /*! + * AND gate. + * Fails if all children have failed. + */ template class DFTAnd : public DFTGate { - + public: - DFTAnd(size_t id, std::string const& name, std::vector>> const& children = {}) : - DFTGate(id, name, children) - {} + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param children Children. + */ + DFTAnd(size_t id, std::string const& name, std::vector>> const& children = {}) : DFTGate(id, name, children) { + // Intentionally empty + } + + DFTElementType type() const override { + return DFTElementType::AND; + } void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - if(state.isOperational(this->mId)) { - for(auto const& child : this->mChildren) - { - if(!state.hasFailed(child->id())) { + if (state.isOperational(this->mId)) { + for (auto const& child : this->mChildren) { + if (!state.hasFailed(child->id())) { return; } } + // All children have failed this->fail(state, queues); } } void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child."); - if(state.isOperational(this->mId)) { + if (state.isOperational(this->mId)) { this->failsafe(state, queues); this->childrenDontCare(state, queues); } } - virtual DFTElementType type() const override { - return DFTElementType::AND; - } - - std::string typestring() const override { - return "AND"; - } }; - + } } diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h index 912c4b42b..38eeb4de1 100644 --- a/src/storm-dft/storage/dft/elements/DFTBE.h +++ b/src/storm-dft/storage/dft/elements/DFTBE.h @@ -6,7 +6,8 @@ namespace storm { namespace storage { /*! - * Abstract base class for basic elements (BEs) in DFTs. + * Abstract base class for basic events (BEs) in DFTs. + * BEs are atomic and not further subdivided. */ template class DFTBE : public DFTElement { @@ -36,8 +37,7 @@ namespace storm { * @param dependency Ingoing dependency. */ void addIngoingDependency(std::shared_ptr> const& dependency) { - // TODO write this assertion for n-ary dependencies, probably by adding a method to the dependencies to support this. - //STORM_LOG_ASSERT(e->dependentEvent()->id() == this->id(), "Ids do not match."); + STORM_LOG_ASSERT(dependency->containsDependentEvent(this->id()), "Dependency " << *dependency << " has no dependent BE " << *this << "."); STORM_LOG_ASSERT(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), dependency) == mIngoingDependencies.end(), "Ingoing Dependency " << dependency << " already present."); mIngoingDependencies.push_back(dependency); @@ -69,19 +69,19 @@ namespace storm { } DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); if (elemsInSubtree.empty()) { - // Parent in the subdft, ie it is *not* a subdft + // Parent in the subDFT, i.e., it is *not* a subDFT return; } - for (auto const& incDep : ingoingDependencies()) { - incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); + for (auto const& inDep : ingoingDependencies()) { + inDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); if (elemsInSubtree.empty()) { - // Parent in the subdft, ie it is *not* a subdft + // Parent in the subDFT, i.e., it is *not* a subDFT return; } } } - bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { + bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { if (DFTElement::checkDontCareAnymore(state, queues)) { state.beNoLongerFailable(this->id()); return true; diff --git a/src/storm-dft/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h index b398518ad..2ef183693 100644 --- a/src/storm-dft/storage/dft/elements/DFTDependency.h +++ b/src/storm-dft/storage/dft/elements/DFTDependency.h @@ -1,120 +1,175 @@ #pragma once - #include "DFTElement.h" + namespace storm { namespace storage { - + + /*! + * Dependency gate with probability p. + * If p=1 the gate is a functional dependency (FDEP), otherwise it is a probabilistic dependency (PDEP). + * + * If the trigger event (i.e., the first child) fails, a coin is flipped. + * With probability p the failure is forwarded to all other children. + * With probability 1-p the failure is not forwarded and the dependency has no effect. + * + * The failure forwarding to the children happens in a strict (non-deterministically chosen) order. + */ template class DFTDependency : public DFTElement { using DFTGatePointer = std::shared_ptr>; using DFTBEPointer = std::shared_ptr>; - - protected: - ValueType mProbability; - DFTGatePointer mTriggerEvent; - std::vector mDependentEvents; public: - DFTDependency(size_t id, std::string const& name, ValueType probability) : - DFTElement(id, name), mProbability(probability) - { + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param probability Probability p of failure forwarding. + */ + DFTDependency(size_t id, std::string const& name, ValueType probability) : DFTElement(id, name), mProbability(probability) { + // We cannot assert 0<=p<=1 in general, because ValueType might be RationalFunction. } - virtual ~DFTDependency() {} - - void setTriggerElement(DFTGatePointer const& triggerEvent) { - mTriggerEvent = triggerEvent; - - } - - void setDependentEvents(std::vector const& dependentEvents) { - mDependentEvents = dependentEvents; + DFTElementType type() const override { + return DFTElementType::PDEP; } - + /*! + * Get probability of forwarding the failure. + * @return Probability. + */ ValueType const& probability() const { return mProbability; } + /*! + * Get trigger event, i.e., the first child. + * @return Trigger event. + */ DFTGatePointer const& triggerEvent() const { STORM_LOG_ASSERT(mTriggerEvent, "Trigger does not exist."); return mTriggerEvent; } + /*! + * Set the trigger event, i.e., the first child. + * @param triggerEvent Trigger event. + */ + void setTriggerElement(DFTGatePointer const& triggerEvent) { + mTriggerEvent = triggerEvent; + } + + /*! + * Get dependent events. + * @return Dependent events. + */ std::vector const& dependentEvents() const { - STORM_LOG_ASSERT(mDependentEvents.size() > 0, "Dependent element does not exists."); + STORM_LOG_ASSERT(mDependentEvents.size() > 0, "Dependent event does not exists."); return mDependentEvents; } - DFTElementType type() const override { - return DFTElementType::PDEP; + /*! + * Add dependent event. + * @param dependentEvent Dependent event. + */ + void addDependentEvent(DFTBEPointer const& dependentEvent) { + mDependentEvents.push_back(dependentEvent); } + /*! + * Check whether the given element is a dependent event. + * @param id Id of element to search for. + * @return True iff element was found in dependent events. + */ + bool containsDependentEvent(size_t id) { + auto it = std::find_if(this->mDependentEvents.begin(), this->mDependentEvents.end(), [&id](DFTBEPointer be) -> bool { + return be->id() == id; + }); + return it != this->mDependentEvents.end(); + } + + virtual size_t nrChildren() const override { return 1; } - virtual bool isDependency() const override { + bool isDependency() const override { return true; } - - virtual bool isTypeEqualTo(DFTElement const& other) const override { - if(!DFTElement::isTypeEqualTo(other)) return false; - DFTDependency const& otherDEP= static_cast const&>(other); - return (mProbability == otherDEP.mProbability); + + /*! + * Check whether the dependency is an FDEP, i.e., p=1. + * @return True iff p=1. + */ + bool isFDEP() const { + return storm::utility::isOne(this->probability()); + } + + bool isTypeEqualTo(DFTElement const& other) const override { + if (!DFTElement::isTypeEqualTo(other)) { + return false; + } + auto& otherDEP = static_cast const&>(other); + return this->probability() == otherDEP.probability(); } - virtual void extendSpareModule(std::set& elementsInSpareModule) const override { + void extendSpareModule(std::set& elementsInSpareModule) const override { // Do nothing } - virtual std::vector independentUnit() const override { + std::vector independentUnit() const override { std::set unit = {this->mId}; - for(auto const& depEv : mDependentEvents) { + for (auto const& depEv : mDependentEvents) { depEv->extendUnit(unit); - if(unit.count(mTriggerEvent->id()) != 0) { + if (unit.count(mTriggerEvent->id()) != 0) { return {}; } } return std::vector(unit.begin(), unit.end()); } - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { - if(elemsInSubtree.count(this->id())) return; + void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { + if (elemsInSubtree.count(this->id())) { + return; + } DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if(elemsInSubtree.empty()) { + if (elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } for (auto const& depEv : mDependentEvents) { depEv->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if (elemsInSubtree.empty()) return; + if (elemsInSubtree.empty()) { + return; + } } - if(elemsInSubtree.empty()) { + if (elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - + } - - virtual std::string toString() const override { + + std::string toString() const override { std::stringstream stream; - bool isFDEP = storm::utility::isOne(this->probability()); - stream << "{" << this->name() << "} " << (isFDEP ? "FDEP" : "PDEP") << "(" << this->triggerEvent()->name() << " => { "; - for(auto const& depEv : this->dependentEvents()) { + stream << "{" << this->name() << "} " << (this->isFDEP() ? "FDEP" : "PDEP") << "(" << this->triggerEvent()->name() << " => { "; + for (auto const& depEv : this->dependentEvents()) { stream << depEv->name() << " "; } stream << "}"; - if (!isFDEP) { + if (!this->isFDEP()) { stream << " with probability " << this->probability(); } return stream.str(); } - protected: + private: + ValueType mProbability; + DFTGatePointer mTriggerEvent; + std::vector mDependentEvents; }; diff --git a/src/storm-dft/storage/dft/elements/DFTGate.h b/src/storm-dft/storage/dft/elements/DFTGate.h index 39020f6cc..bbf856b14 100644 --- a/src/storm-dft/storage/dft/elements/DFTGate.h +++ b/src/storm-dft/storage/dft/elements/DFTGate.h @@ -40,7 +40,9 @@ namespace storm { } - virtual std::string typestring() const = 0; + virtual std::string typestring() const { + return storm::storage::toString(this->type()); + } virtual void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; diff --git a/src/storm-dft/storage/dft/elements/DFTOr.h b/src/storm-dft/storage/dft/elements/DFTOr.h index f45bb4b5b..4f5c8b2e0 100644 --- a/src/storm-dft/storage/dft/elements/DFTOr.h +++ b/src/storm-dft/storage/dft/elements/DFTOr.h @@ -1,39 +1,49 @@ -#pragma once +#pragma once #include "DFTGate.h" + namespace storm { namespace storage { + + /*! + * OR gate. + * Fails if at least one child has failed. + */ template class DFTOr : public DFTGate { public: - DFTOr(size_t id, std::string const& name, std::vector>> const& children = {}) : - DFTGate(id, name, children) - {} + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param children Children. + */ + DFTOr(size_t id, std::string const& name, std::vector>> const& children = {}) : DFTGate(id, name, children) { + // Intentionally empty + } + + DFTElementType type() const override { + return DFTElementType::OR; + } void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { STORM_LOG_ASSERT(this->hasFailedChild(state), "No failed child."); - if(state.isOperational(this->mId)) { + if (state.isOperational(this->mId)) { this->fail(state, queues); } } void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - for(auto const& child : this->mChildren) { - if(!state.isFailsafe(child->id())) { - return; - } - } - this->failsafe(state, queues); + for (auto const& child : this->mChildren) { + if (!state.isFailsafe(child->id())) { + return; + } + } + // All chidren are failsafe + this->failsafe(state, queues); } - virtual DFTElementType type() const override { - return DFTElementType::OR; - } - - std::string typestring() const override { - return "OR"; - } }; } diff --git a/src/storm-dft/storage/dft/elements/DFTPand.h b/src/storm-dft/storage/dft/elements/DFTPand.h index 7b03b7196..33ad6c399 100644 --- a/src/storm-dft/storage/dft/elements/DFTPand.h +++ b/src/storm-dft/storage/dft/elements/DFTPand.h @@ -1,57 +1,78 @@ -#pragma once +#pragma once #include "DFTGate.h" + namespace storm { namespace storage { - template + + /*! + * Priority AND (PAND) gate. + * Fails if all children fail in order from first to last child. + * If a child fails before its left sibling, the PAND becomes failsafe. + * For inclusive PAND<= gates, simultaneous failures are allowed. + * For exclusive PAND< gates, simultaneous failure make the gate failsafe. + */ + template class DFTPand : public DFTGate { public: - DFTPand(size_t id, std::string const& name, bool inclusive, std::vector>> const& children = {}) : - DFTGate(id, name, children), - inclusive(inclusive) - {} - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - assert(inclusive); - if(state.isOperational(this->mId)) { + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param inclusive If true, simultaneous failures are allowed. + * parame children Children. + */ + DFTPand(size_t id, std::string const& name, bool inclusive, std::vector>> const& children = {}) : DFTGate(id, name, children), inclusive(inclusive) { + // Intentionally left empty. + } + + DFTElementType type() const override { + return DFTElementType::PAND; + } + + std::string typestring() const override { + return isInclusive() ? "PAND (incl)" : "PAND (excl)"; + } + + /*! + * Return whether the PAND is inclusive. + * @return True iff PAND is inclusive. + */ + bool isInclusive() const { + return inclusive; + } + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + STORM_LOG_ASSERT(isInclusive(), "Exclusive PAND not supported."); + if (state.isOperational(this->mId)) { bool childOperationalBefore = false; - for(auto const& child : this->mChildren) - { - if(!state.hasFailed(child->id())) { + for (auto const& child : this->mChildren) { + if (!state.hasFailed(child->id())) { childOperationalBefore = true; - } else if(childOperationalBefore && state.hasFailed(child->id())){ + } else if (childOperationalBefore && state.hasFailed(child->id())) { + // Child failed before sibling -> failsafe this->failsafe(state, queues); this->childrenDontCare(state, queues); return; } } - if(!childOperationalBefore) { + if (!childOperationalBefore) { + // All children have failed this->fail(state, queues); } } } void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - assert(inclusive); + STORM_LOG_ASSERT(isInclusive(), "Exclusive PAND not supported."); STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child."); - if(state.isOperational(this->mId)) { + if (state.isOperational(this->mId)) { this->failsafe(state, queues); this->childrenDontCare(state, queues); } } - virtual DFTElementType type() const override { - return DFTElementType::PAND; - } - - bool isInclusive() const { - return inclusive; - } - - std::string typestring() const override { - return inclusive ? "PAND-inc" : "PAND-ex"; - } protected: bool inclusive; }; diff --git a/src/storm-dft/storage/dft/elements/DFTPor.h b/src/storm-dft/storage/dft/elements/DFTPor.h index 1e92384cd..885cc7300 100644 --- a/src/storm-dft/storage/dft/elements/DFTPor.h +++ b/src/storm-dft/storage/dft/elements/DFTPor.h @@ -1,53 +1,76 @@ -#pragma once +#pragma once #include "DFTGate.h" + namespace storm { namespace storage { + + /*! + * Priority OR (POR) gate. + * Fails if the leftmost child fails before all other children. + * If a child fails before the leftmost child, the POR becomes failsafe. + * For inclusive POR<= gates, simultaneous failures are allowed. + * For exclusive POR< gates, simultaneous failures make the gate failsafe. + */ template class DFTPor : public DFTGate { public: - DFTPor(size_t id, std::string const& name, bool inclusive, std::vector>> const& children = {}) : - DFTGate(id, name, children), - inclusive(inclusive) - {} - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - assert(inclusive); - if(state.isOperational(this->mId)) { - if (state.hasFailed(this->mChildren.front()->id())) { + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param inclusive If true, simultaneous failures are allowed. + * parame children Children. + */ + DFTPor(size_t id, std::string const& name, bool inclusive, std::vector>> const& children = {}) : DFTGate(id, name, children), inclusive(inclusive) { + // Intentionally left empty. + } + + DFTElementType type() const override { + return DFTElementType::POR; + } + + std::string typestring() const override { + return isInclusive() ? "POR (incl)" : "POR (excl)"; + } + + /*! + * Return whether the PAND is inclusive. + * @return True iff PAND is inclusive. + */ + bool isInclusive() const { + return inclusive; + } + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { + STORM_LOG_ASSERT(isInclusive(), "Exclusive POR not supported."); + if (state.isOperational(this->mId)) { + auto childIter = this->mChildren.begin(); + if (state.hasFailed((*childIter)->id())) { // First child has failed before others this->fail(state, queues); - } else { - for (size_t i = 1; i < this->nrChildren(); ++i) { - if (state.hasFailed(this->mChildren[i]->id())) { - // Child has failed before first child - this->failsafe(state, queues); - this->childrenDontCare(state, queues); - } + return; + } + // Iterate over other children + for (; childIter != this->mChildren.end(); ++childIter) { + if (state.hasFailed((*childIter)->id())) { + // Child has failed before first child + this->failsafe(state, queues); + this->childrenDontCare(state, queues); } } } } void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - assert(inclusive); + STORM_LOG_ASSERT(isInclusive(), "Exclusive POR not supported."); + // If first child is not failsafe, it could still fail. if (state.isFailsafe(this->mChildren.front()->id())) { this->failsafe(state, queues); this->childrenDontCare(state, queues); } } - virtual DFTElementType type() const override { - return DFTElementType::POR; - } - - std::string typestring() const override { - return inclusive ? "POR-inc" : "POR-ex"; - } - - bool isInclusive() const { - return inclusive; - } protected: bool inclusive; }; diff --git a/src/storm-dft/storage/dft/elements/DFTVot.h b/src/storm-dft/storage/dft/elements/DFTVot.h index 791926a97..bb40998ac 100644 --- a/src/storm-dft/storage/dft/elements/DFTVot.h +++ b/src/storm-dft/storage/dft/elements/DFTVot.h @@ -1,48 +1,70 @@ -#pragma once +#pragma once + #include "DFTGate.h" + namespace storm { namespace storage { - + /*! + * VOT gate with threshold k. + * Fails if k children have failed. + */ template class DFTVot : public DFTGate { - private: - unsigned mThreshold; - public: - DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector>> const& children = {}) : - DFTGate(id, name, children), mThreshold(threshold) - {} + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param threshold Threshold k, nr of failed children needed for failure. + * @param children Children. + */ + DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector>> const& children = {}) : DFTGate(id, name, children), mThreshold(threshold) { + STORM_LOG_ASSERT(mThreshold > 1, "Should use OR gate instead of VOT1"); + // k=n cannot be checked as children might be added later + } + + /*! + * Get the threshold k. + * @return Threshold. + */ + unsigned threshold() const { + return mThreshold; + } + + DFTElementType type() const override { + return DFTElementType::VOT; + } + + std::string typestring() const override { + return storm::storage::toString(this->type()) + " (" + std::to_string(mThreshold) + ")"; + } void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - if(state.isOperational(this->mId)) { + if (state.isOperational(this->mId)) { unsigned nrFailedChildren = 0; - for(auto const& child : this->mChildren) - { - if(state.hasFailed(child->id())) { + for (auto const& child : this->mChildren) { + if (state.hasFailed(child->id())) { ++nrFailedChildren; - if(nrFailedChildren >= mThreshold) - { + if (nrFailedChildren >= mThreshold) { this->fail(state, queues); return; } } } - - } + + } } void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child."); - if(state.isOperational(this->mId)) { + if (state.isOperational(this->mId)) { unsigned nrFailsafeChildren = 0; - for(auto const& child : this->mChildren) - { - if(state.isFailsafe(child->id())) { + for (auto const& child : this->mChildren) { + if (state.isFailsafe(child->id())) { ++nrFailsafeChildren; - if(nrFailsafeChildren > this->nrChildren() - mThreshold) - { + if (nrFailsafeChildren > this->nrChildren() - mThreshold) { this->failsafe(state, queues); this->childrenDontCare(state, queues); return; @@ -51,24 +73,18 @@ namespace storm { } } } - - unsigned threshold() const { - return mThreshold; - } - virtual DFTElementType type() const override { - return DFTElementType::VOT; - } - - std::string typestring() const override{ - return "VOT (" + std::to_string(mThreshold) + ")"; - } - - virtual bool isTypeEqualTo(DFTElement const& other) const override { - if(!DFTElement::isTypeEqualTo(other)) return false; - DFTVot const& otherVOT = static_cast const&>(other); - return (mThreshold == otherVOT.mThreshold); + bool isTypeEqualTo(DFTElement const& other) const override { + if (!DFTElement::isTypeEqualTo(other)) { + return false; + } + auto& otherVOT = static_cast const&>(other); + return this->threshold() == otherVOT.threshold(); } + + private: + unsigned mThreshold; + }; }