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<typename ValueType>
class BEConst : public DFTBE<ValueType> {
@@ -38,7 +39,7 @@ namespace storm {
return this->failed();
}
- bool isTypeEqualTo(DFTElement <ValueType> const& other) const override {
+ bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
if (!DFTElement<ValueType>::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 <ValueType> const& other) const override {
+ bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
if (!DFTElement<ValueType>::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<typename ValueType>
class DFTAnd : public DFTGate<ValueType> {
-
+
public:
- DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
- {}
+ /*!
+ * Constructor.
+ * @param id Id.
+ * @param name Name.
+ * @param children Children.
+ */
+ DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTGate<ValueType>(id, name, children) {
+ // Intentionally empty
+ }
+
+ DFTElementType type() const override {
+ return DFTElementType::AND;
+ }
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<typename ValueType>
class DFTBE : public DFTElement<ValueType> {
@@ -36,8 +37,7 @@ namespace storm {
* @param dependency Ingoing dependency.
*/
void addIngoingDependency(std::shared_ptr<DFTDependency<ValueType>> 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<ValueType>::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<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
+ bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
if (DFTElement<ValueType>::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<typename ValueType>
class DFTDependency : public DFTElement<ValueType> {
using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
using DFTBEPointer = std::shared_ptr<DFTBE<ValueType>>;
-
- protected:
- ValueType mProbability;
- DFTGatePointer mTriggerEvent;
- std::vector<DFTBEPointer> mDependentEvents;
public:
- DFTDependency(size_t id, std::string const& name, ValueType probability) :
- DFTElement<ValueType>(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<ValueType>(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<DFTBEPointer> 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<DFTBEPointer> 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<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);
+
+ /*!
+ * 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<ValueType> const& other) const override {
+ if (!DFTElement<ValueType>::isTypeEqualTo(other)) {
+ return false;
+ }
+ auto& otherDEP = static_cast<DFTDependency<ValueType> const&>(other);
+ return this->probability() == otherDEP.probability();
}
- virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
+ void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
// Do nothing
}
- virtual std::vector<size_t> independentUnit() const override {
+ std::vector<size_t> independentUnit() const override {
std::set<size_t> 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<size_t>(unit.begin(), unit.end());
}
- virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
- if(elemsInSubtree.count(this->id())) return;
+ void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
+ if (elemsInSubtree.count(this->id())) {
+ return;
+ }
DFTElement<ValueType>::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<DFTBEPointer> 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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<typename ValueType>
class DFTOr : public DFTGate<ValueType> {
public:
- DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
- {}
+ /*!
+ * Constructor.
+ * @param id Id.
+ * @param name Name.
+ * @param children Children.
+ */
+ DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTGate<ValueType>(id, name, children) {
+ // Intentionally empty
+ }
+
+ DFTElementType type() const override {
+ return DFTElementType::OR;
+ }
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<typename ValueType>
+
+ /*!
+ * 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<typename ValueType>
class DFTPand : public DFTGate<ValueType> {
public:
- DFTPand(size_t id, std::string const& name, bool inclusive, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children),
- inclusive(inclusive)
- {}
-
- void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTGate<ValueType>(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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<typename ValueType>
class DFTPor : public DFTGate<ValueType> {
public:
- DFTPor(size_t id, std::string const& name, bool inclusive, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children),
- inclusive(inclusive)
- {}
-
- void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTGate<ValueType>(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<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& 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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<typename ValueType>
class DFTVot : public DFTGate<ValueType> {
- private:
- unsigned mThreshold;
-
public:
- DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(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<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTGate<ValueType>(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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<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);
+ bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+ if (!DFTElement<ValueType>::isTypeEqualTo(other)) {
+ return false;
+ }
+ auto& otherVOT = static_cast<DFTVot<ValueType> const&>(other);
+ return this->threshold() == otherVOT.threshold();
}
+
+ private:
+ unsigned mThreshold;
+
};
}