diff --git a/src/storm-dft/storage/dft/DFTElements.h b/src/storm-dft/storage/dft/DFTElements.h index 42aaa4b18..3173446fb 100644 --- a/src/storm-dft/storage/dft/DFTElements.h +++ b/src/storm-dft/storage/dft/DFTElements.h @@ -1,10 +1,9 @@ #pragma once -#include "storm-dft/storage/dft/elements/DFTAnd.h" -#include "storm-dft/storage/dft/elements/DFTBE.h" +#include "storm-dft/storage/dft/elements/BEExponential.h" #include "storm-dft/storage/dft/elements/BEConst.h" +#include "storm-dft/storage/dft/elements/DFTAnd.h" #include "storm-dft/storage/dft/elements/DFTDependency.h" -#include "storm-dft/storage/dft/elements/BEExponential.h" #include "storm-dft/storage/dft/elements/DFTOr.h" #include "storm-dft/storage/dft/elements/DFTPand.h" #include "storm-dft/storage/dft/elements/DFTPor.h" diff --git a/src/storm-dft/storage/dft/elements/DFTChildren.h b/src/storm-dft/storage/dft/elements/DFTChildren.h new file mode 100644 index 000000000..5a0e53776 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/DFTChildren.h @@ -0,0 +1,167 @@ +#pragma once + +#include "DFTElement.h" + +namespace storm { + namespace storage { + + /*! + * Abstract base class for a DFT element with children. + */ + template + class DFTChildren : public DFTElement { + + using DFTElementPointer = std::shared_ptr>; + using DFTElementVector = std::vector; + + public: + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param children Children. + */ + DFTChildren(size_t id, std::string const& name, DFTElementVector const& children) : DFTElement(id, name), mChildren(children) { + // Intentionally left empty. + } + + /*! + * Destructor. + */ + virtual ~DFTChildren() { + // Intentionally left empty. + } + + /*! + * Add child. + * @param element Element. + */ + void pushBackChild(DFTElementPointer element) { + mChildren.push_back(element); + } + + /*! + * Get children. + * @return Children. + */ + DFTElementVector const& children() const { + return mChildren; + } + + size_t nrChildren() const override { + return mChildren.size(); + } + + virtual std::vector independentUnit() const override { + std::set unit = {this->mId}; + for (auto const& child : mChildren) { + child->extendUnit(unit); + } + 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(bool blockParents, bool sparesAsLeaves = false) const override { + auto prelRes = DFTElement::independentSubDft(blockParents); + 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, blockParents, sparesAsLeaves); + 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, bool blockParents, bool sparesAsLeaves) const override { + if (elemsInSubtree.count(this->id()) > 0) return; + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); + if (elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + for (auto const& child : mChildren) { + child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); + if (elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + } + } + + /*! + * Check failed status. + * @param state Current state of DFT. + * @param queues Propagation queue for failed. + */ + virtual void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; + + /*! + * Check failsafe status. + * @param state Current state of DFT. + * @param queues Propagation queue for failsafe. + */ + virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; + + virtual std::string toString() const override { + std::stringstream stream; + stream << "{" << this->name() << "} " << this->typestring() << "( "; + typename DFTElementVector::const_iterator it = mChildren.begin(); + stream << (*it)->name(); + ++it; + while (it != mChildren.end()) { + stream << ", " << (*it)->name(); + ++it; + } + stream << ")"; + return stream.str(); + } + + protected: + /*! + * Check whether it has a failsafe child. + * @param state Current state of DFT. + * @return True iff failsafe child exists. + */ + bool hasFailsafeChild(DFTState& state) const { + for (auto const& child : mChildren) { + if (state.isFailsafe(child->id())) { + return true; + } + } + return false; + } + + /*! + * Check whether it has a failed child. + * @param state Current state of DFT. + * @return True iff failed child exists. + */ + bool hasFailedChild(DFTState& state) const { + for (auto const& child : mChildren) { + if (state.hasFailed(child->id())) { + return true; + } + } + return false; + } + + private: + DFTElementVector mChildren; + + }; + + } +} diff --git a/src/storm-dft/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h index 2ef183693..c055c119f 100644 --- a/src/storm-dft/storage/dft/elements/DFTDependency.h +++ b/src/storm-dft/storage/dft/elements/DFTDependency.h @@ -32,10 +32,21 @@ namespace storm { // We cannot assert 0<=p<=1 in general, because ValueType might be RationalFunction. } + /*! + * Destructor + */ + virtual ~DFTDependency() { + // Intentionally left empty. + }; + DFTElementType type() const override { return DFTElementType::PDEP; } + std::string typestring() const override { + return this->isFDEP() ? "FDEP" : "PDEP"; + } + /*! * Get probability of forwarding the failure. * @return Probability. @@ -155,7 +166,7 @@ namespace storm { std::string toString() const override { std::stringstream stream; - stream << "{" << this->name() << "} " << (this->isFDEP() ? "FDEP" : "PDEP") << "(" << this->triggerEvent()->name() << " => { "; + stream << "{" << this->name() << "} " << this->typestring() << "(" << this->triggerEvent()->name() << " => { "; for (auto const& depEv : this->dependentEvents()) { stream << depEv->name() << " "; } diff --git a/src/storm-dft/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h index 2c43bdab8..5690f5f0c 100644 --- a/src/storm-dft/storage/dft/elements/DFTElement.h +++ b/src/storm-dft/storage/dft/elements/DFTElement.h @@ -99,6 +99,10 @@ namespace storm { */ virtual DFTElementType type() const = 0; + virtual std::string typestring() const { + return storm::storage::toString(this->type()); + } + /*! * Get rank. * @return Rank. @@ -290,7 +294,10 @@ namespace storm { virtual void extendSpareModule(std::set& elementsInModule) const; // virtual void extendImmediateFailureCausePathEvents(std::set& ) const; - + /*! + * Get number of children. + * @return Nr of children. + */ virtual std::size_t nrChildren() const = 0; virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; diff --git a/src/storm-dft/storage/dft/elements/DFTGate.h b/src/storm-dft/storage/dft/elements/DFTGate.h index bbf856b14..a41a14ae8 100644 --- a/src/storm-dft/storage/dft/elements/DFTGate.h +++ b/src/storm-dft/storage/dft/elements/DFTGate.h @@ -1,10 +1,15 @@ #pragma once -#include "DFTElement.h" +#include "DFTChildren.h" + namespace storm { namespace storage { - template - class DFTGate : public DFTElement { + + /*! + * Abstract base class for gates. + */ + template + class DFTGate : public DFTChildren { using DFTElementPointer = std::shared_ptr>; using DFTElementVector = std::vector; @@ -13,41 +18,35 @@ namespace storm { DFTElementVector mChildren; public: - DFTGate(size_t id, std::string const& name, DFTElementVector const& children) : - DFTElement(id, name), mChildren(children) - {} - - virtual ~DFTGate() {} - - void pushBackChild(DFTElementPointer elem) { - return mChildren.push_back(elem); + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param children Children. + */ + DFTGate(size_t id, std::string const& name, DFTElementVector const& children) : DFTChildren(id, name, children) { + // Intentionally left empty. } - size_t nrChildren() const override { - return mChildren.size(); + /*! + * Destructor + */ + virtual ~DFTGate() { + // Intentionally left empty. } - DFTElementVector const& children() const { - return mChildren; - } - virtual bool isGate() const override { return true; } - + + /*! + * Return whether the gate is a dynamic gate. + * @return True iff the gate is dynamic. + */ bool isDynamicGate() const { return !isStaticGateType(this->type()); } - - - virtual std::string typestring() const { - return storm::storage::toString(this->type()); - } - virtual void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; - - virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; - virtual void extendSpareModule(std::set& elementsInSpareModule) const override { if (!this->isSpareGate()) { DFTElement::extendSpareModule(elementsInSpareModule); @@ -59,73 +58,9 @@ namespace storm { } } } - - virtual std::vector independentUnit() const override { - std::set unit = {this->mId}; - for(auto const& child : mChildren) { - child->extendUnit(unit); - } - 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(bool blockParents, bool sparesAsLeaves = false) const override { - auto prelRes = DFTElement::independentSubDft(blockParents); - 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, blockParents, sparesAsLeaves); - 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, bool blockParents, bool sparesAsLeaves) const override { - if(elemsInSubtree.count(this->id()) > 0) return; - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if(elemsInSubtree.empty()) { - // Parent in the subdft, ie it is *not* a subdft - return; - } - for(auto const& child : mChildren) { - child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if(elemsInSubtree.empty()) { - // Parent in the subdft, ie it is *not* a subdft - return; - } - } - } - - - virtual std::string toString() const override { - std::stringstream stream; - stream << "{" << this->name() << "} " << typestring() << "( "; - typename DFTElementVector::const_iterator it = mChildren.begin(); - stream << (*it)->name(); - ++it; - while(it != mChildren.end()) { - stream << ", " << (*it)->name(); - ++it; - } - stream << ")"; - return stream.str(); - } virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - if(DFTElement::checkDontCareAnymore(state, queues)) { + if (DFTElement::checkDontCareAnymore(state, queues)) { childrenDontCare(state, queues); return true; } @@ -136,12 +71,12 @@ namespace storm { protected: void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - for(std::shared_ptr parent : this->mParents) { - if(state.isOperational(parent->id())) { + for (std::shared_ptr parent : this->mParents) { + if (state.isOperational(parent->id())) { queues.propagateFailure(parent); } } - for(std::shared_ptr> restr : this->mRestrictions) { + for (std::shared_ptr> restr : this->mRestrictions) { queues.checkRestrictionLater(restr); } state.setFailed(this->mId); @@ -149,38 +84,19 @@ namespace storm { } void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - for(std::shared_ptr parent : this->mParents) { - if(state.isOperational(parent->id())) { + for (std::shared_ptr parent : this->mParents) { + if (state.isOperational(parent->id())) { queues.propagateFailsafe(parent); } } state.setFailsafe(this->mId); this->childrenDontCare(state, queues); } - + void childrenDontCare(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { queues.propagateDontCare(mChildren); } - - bool hasFailsafeChild(DFTState& state) const { - for(auto const& child : mChildren) { - if(state.isFailsafe(child->id())) - { - return true; - } - } - return false; - } - - bool hasFailedChild(DFTState& state) const { - for(auto const& child : mChildren) { - if(state.hasFailed(child->id())) { - return true; - } - } - return false; - } - }; + } } diff --git a/src/storm-dft/storage/dft/elements/DFTPand.h b/src/storm-dft/storage/dft/elements/DFTPand.h index 33ad6c399..70352332f 100644 --- a/src/storm-dft/storage/dft/elements/DFTPand.h +++ b/src/storm-dft/storage/dft/elements/DFTPand.h @@ -24,7 +24,7 @@ namespace storm { * 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. + // Intentionally left empty. } DFTElementType type() const override { @@ -32,7 +32,7 @@ namespace storm { } std::string typestring() const override { - return isInclusive() ? "PAND (incl)" : "PAND (excl)"; + return this->isInclusive() ? "PAND (incl)" : "PAND (excl)"; } /*! diff --git a/src/storm-dft/storage/dft/elements/DFTPor.h b/src/storm-dft/storage/dft/elements/DFTPor.h index 885cc7300..617290bca 100644 --- a/src/storm-dft/storage/dft/elements/DFTPor.h +++ b/src/storm-dft/storage/dft/elements/DFTPor.h @@ -31,7 +31,7 @@ namespace storm { } std::string typestring() const override { - return isInclusive() ? "POR (incl)" : "POR (excl)"; + return this->isInclusive() ? "POR (incl)" : "POR (excl)"; } /*! @@ -42,7 +42,7 @@ namespace storm { return inclusive; } - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { + 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(); diff --git a/src/storm-dft/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h index 10392e05c..d1a69c98b 100644 --- a/src/storm-dft/storage/dft/elements/DFTRestriction.h +++ b/src/storm-dft/storage/dft/elements/DFTRestriction.h @@ -1,44 +1,55 @@ #pragma once -#include "DFTElement.h" +#include "DFTChildren.h" + namespace storm { namespace storage { + + /*! + * Abstract base class for restrictions. + * Restrictions prevent the failure of DFT events. + */ template - class DFTRestriction : public DFTElement { + class DFTRestriction : public DFTChildren { using DFTElementPointer = std::shared_ptr>; using DFTElementVector = std::vector; - protected: - DFTElementVector mChildren; public: - DFTRestriction(size_t id, std::string const& name, DFTElementVector const& children) : - DFTElement(id, name), mChildren(children) - {} - - virtual ~DFTRestriction() {} - - void pushBackChild(DFTElementPointer elem) { - return mChildren.push_back(elem); - } - - size_t nrChildren() const override { - return mChildren.size(); - } - - DFTElementVector const& children() const { - return mChildren; - } - - virtual bool isRestriction() const override { + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param children Children. + */ + DFTRestriction(size_t id, std::string const& name, DFTElementVector const& children) : DFTChildren(id, name, children) { + // Intentionally left empty. + } + + /*! + * Destructor + */ + virtual ~DFTRestriction() { + // Intentionally left empty. + }; + + bool isRestriction() const override { return true; } - + + /*! + * Return whether the restriction is a sequence enforcer. + * @return True iff the restriction is a SEQ. + */ virtual bool isSeqEnforcer() const { return false; } - + + /*! + * Returns whether all children are BEs. + * @return True iff all children are BEs. + */ bool allChildrenBEs() const { - for(auto const& elem : mChildren) { + for (auto const& elem : mChildren) { if (!elem->isBasicElement()) { return false; } @@ -46,165 +57,75 @@ namespace storm { return true; } - - virtual std::string typestring() const = 0; - - virtual void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; - - virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; - virtual void extendSpareModule(std::set& elementsInSpareModule) const override { // Do nothing } - virtual std::vector independentUnit() const override { - std::set unit = {this->mId}; - for(auto const& child : mChildren) { - child->extendUnit(unit); - } - 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(bool blockParents, bool sparesAsLeaves) const override { - auto prelRes = DFTElement::independentSubDft(blockParents); - 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, blockParents, sparesAsLeaves); - 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, bool blockParents, bool sparesAsLeaves) const override { - if(elemsInSubtree.count(this->id()) > 0) return; - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if(elemsInSubtree.empty()) { - // Parent in the subdft, ie it is *not* a subdft - return; - } - for(auto const& child : mChildren) { - child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if(elemsInSubtree.empty()) { - // Parent in the subdft, ie it is *not* a subdft - return; - } - } - } - - virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { return false; } protected: - - void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + void fail(DFTState & state, DFTStateSpaceGenerationQueues & queues) const { state.markAsInvalid(); } - void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + void failsafe(DFTState & state, DFTStateSpaceGenerationQueues & queues) const { } - bool hasFailsafeChild(DFTState& state) const { - for(auto const& child : mChildren) { - if(state.isFailsafe(child->id())) - { - return true; - } - } - return false; - } - - bool hasFailedChild(DFTState& state) const { - for(auto const& child : mChildren) { - if(state.hasFailed(child->id())) { - return true; - } - } - return false; - } - - virtual std::string toString() const override { - std::stringstream stream; - stream << "{" << this->name() << "} " << this->typestring() << "( "; - auto it = this->children().begin(); - stream << (*it)->name(); - ++it; - while(it != this->children().end()) { - stream << ", " << (*it)->name(); - ++it; - } - stream << ")"; - return stream.str(); - } - - + DFTElementVector mChildren; }; + /*! + * Sequence enforcer (SEQ). + * All children can only fail in order from first to last child. + * A child which has not failed yet prevents the failure of all children to the right of it. + */ template class DFTSeq : public DFTRestriction { - public: - DFTSeq(size_t id, std::string const& name, std::vector>> const& children = {}) : - DFTRestriction(id, name, children) - {} + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param children Children. + */ + DFTSeq(size_t id, std::string const& name, std::vector>> const&children = {}) : DFTRestriction(id, name, children) { + // Intentionally left empty. + } + + virtual DFTElementType type() const override { + return DFTElementType::SEQ; + } virtual bool isSeqEnforcer() const override { return true; } - - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { STORM_LOG_ASSERT(queues.failurePropagationDone(), "Failure propagation not finished."); 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())) { this->fail(state, queues); return; } } - } - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - - + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { } - - virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + + virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { // Actually, it doesnt matter what we return here.. return false; } - - virtual DFTElementType type() const override { - return DFTElementType::SEQ; - } - - std::string typestring() const override { - return "SEQ"; - } }; }