diff --git a/src/storm-dft/storage/dft/elements/DFTAnd.h b/src/storm-dft/storage/dft/elements/DFTAnd.h
index aab72d436..6c1108c66 100644
--- a/src/storm-dft/storage/dft/elements/DFTAnd.h
+++ b/src/storm-dft/storage/dft/elements/DFTAnd.h
@@ -29,7 +29,7 @@ namespace storm {
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
if (state.isOperational(this->mId)) {
- for (auto const& child : this->mChildren) {
+ for (auto const& child : this->children()) {
if (!state.hasFailed(child->id())) {
return;
}
diff --git a/src/storm-dft/storage/dft/elements/DFTGate.h b/src/storm-dft/storage/dft/elements/DFTGate.h
index a41a14ae8..1c3000c85 100644
--- a/src/storm-dft/storage/dft/elements/DFTGate.h
+++ b/src/storm-dft/storage/dft/elements/DFTGate.h
@@ -14,9 +14,6 @@ namespace storm {
using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
using DFTElementVector = std::vector<DFTElementPointer>;
- protected:
- DFTElementVector mChildren;
-
public:
/*!
* Constructor.
@@ -50,7 +47,7 @@ namespace storm {
virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
if (!this->isSpareGate()) {
DFTElement<ValueType>::extendSpareModule(elementsInSpareModule);
- for (auto const& child : mChildren) {
+ for (auto const& child : this->children()) {
if (elementsInSpareModule.count(child->id()) == 0) {
elementsInSpareModule.insert(child->id());
child->extendSpareModule(elementsInSpareModule);
@@ -70,7 +67,7 @@ namespace storm {
protected:
- void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+ virtual void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
for (std::shared_ptr<DFTGate> parent : this->mParents) {
if (state.isOperational(parent->id())) {
queues.propagateFailure(parent);
@@ -83,7 +80,7 @@ namespace storm {
this->childrenDontCare(state, queues);
}
- void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+ virtual void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
for (std::shared_ptr<DFTGate> parent : this->mParents) {
if (state.isOperational(parent->id())) {
queues.propagateFailsafe(parent);
@@ -94,7 +91,7 @@ namespace storm {
}
void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
- queues.propagateDontCare(mChildren);
+ queues.propagateDontCare(this->children());
}
};
diff --git a/src/storm-dft/storage/dft/elements/DFTOr.h b/src/storm-dft/storage/dft/elements/DFTOr.h
index 4f5c8b2e0..de0225cea 100644
--- a/src/storm-dft/storage/dft/elements/DFTOr.h
+++ b/src/storm-dft/storage/dft/elements/DFTOr.h
@@ -35,7 +35,7 @@ namespace storm {
}
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- for (auto const& child : this->mChildren) {
+ for (auto const& child : this->children()) {
if (!state.isFailsafe(child->id())) {
return;
}
diff --git a/src/storm-dft/storage/dft/elements/DFTPand.h b/src/storm-dft/storage/dft/elements/DFTPand.h
index 70352332f..1eaa0a9e7 100644
--- a/src/storm-dft/storage/dft/elements/DFTPand.h
+++ b/src/storm-dft/storage/dft/elements/DFTPand.h
@@ -47,7 +47,7 @@ namespace storm {
STORM_LOG_ASSERT(isInclusive(), "Exclusive PAND not supported.");
if (state.isOperational(this->mId)) {
bool childOperationalBefore = false;
- for (auto const& child : this->mChildren) {
+ for (auto const& child : this->children()) {
if (!state.hasFailed(child->id())) {
childOperationalBefore = true;
} else if (childOperationalBefore && state.hasFailed(child->id())) {
diff --git a/src/storm-dft/storage/dft/elements/DFTPor.h b/src/storm-dft/storage/dft/elements/DFTPor.h
index 617290bca..11a8a25a6 100644
--- a/src/storm-dft/storage/dft/elements/DFTPor.h
+++ b/src/storm-dft/storage/dft/elements/DFTPor.h
@@ -45,14 +45,14 @@ namespace storm {
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();
+ auto childIter = this->children().begin();
if (state.hasFailed((*childIter)->id())) {
// First child has failed before others
this->fail(state, queues);
return;
}
// Iterate over other children
- for (; childIter != this->mChildren.end(); ++childIter) {
+ for (; childIter != this->children().end(); ++childIter) {
if (state.hasFailed((*childIter)->id())) {
// Child has failed before first child
this->failsafe(state, queues);
@@ -65,7 +65,7 @@ namespace storm {
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
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())) {
+ if (state.isFailsafe(this->children().front()->id())) {
this->failsafe(state, queues);
this->childrenDontCare(state, queues);
}
diff --git a/src/storm-dft/storage/dft/elements/DFTSpare.h b/src/storm-dft/storage/dft/elements/DFTSpare.h
index 7584a1f94..52097f701 100644
--- a/src/storm-dft/storage/dft/elements/DFTSpare.h
+++ b/src/storm-dft/storage/dft/elements/DFTSpare.h
@@ -1,41 +1,45 @@
-#pragma once
-
+#pragma once
#include "DFTGate.h"
+
namespace storm {
namespace storage {
-
+ /*!
+ * SPARE gate.
+ */
template<typename ValueType>
class DFTSpare : public DFTGate<ValueType> {
public:
- DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
- {}
-
- std::string typestring() const override {
- return "SPARE";
+ /*!
+ * Constructor.
+ * @param id Id.
+ * @param name Name.
+ * @param children Children.
+ */
+ DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTGate<ValueType>(id, name, children) {
+ // Intentionally left empty.
}
- virtual DFTElementType type() const override {
+ DFTElementType type() const override {
return DFTElementType::SPARE;
}
bool isSpareGate() const override {
return true;
}
-
- void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+
+ void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
DFTGate<ValueType>::fail(state, queues);
state.finalizeUses(this->mId);
}
-
- void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+
+ void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
DFTGate<ValueType>::failsafe(state, queues);
state.finalizeUses(this->mId);
}
-
+
bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
if (DFTGate<ValueType>::checkDontCareAnymore(state, queues)) {
state.finalizeUses(this->mId);
@@ -43,40 +47,40 @@ namespace storm {
}
return false;
}
-
+
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- if(state.isOperational(this->mId)) {
+ if (state.isOperational(this->mId)) {
size_t uses = state.uses(this->mId);
- if(!state.isOperational(uses)) {
- bool claimingSuccessful = state.claimNew(this->mId, uses, this->mChildren);
- if(!claimingSuccessful) {
+ if (!state.isOperational(uses)) {
+ bool claimingSuccessful = state.claimNew(this->mId, uses, this->children());
+ if (!claimingSuccessful) {
this->fail(state, queues);
}
- }
- }
+ }
+ }
}
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- if(state.isOperational(this->mId)) {
- if(state.isFailsafe(state.uses(this->mId))) {
+ if (state.isOperational(this->mId)) {
+ if (state.isFailsafe(state.uses(this->mId))) {
this->failsafe(state, queues);
this->childrenDontCare(state, queues);
}
}
}
-
+
std::vector<size_t> independentSubDft(bool blockParents, bool sparesAsLeaves = false) const override {
auto prelRes = DFTElement<ValueType>::independentSubDft(blockParents);
- if(prelRes.empty()) {
+ 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<size_t> unit(prelRes.begin(), prelRes.end());
std::vector<size_t> pids = this->parentIds();
if (!sparesAsLeaves) {
- for(auto const& child : this->mChildren) {
+ for (auto const& child : this->children()) {
child->extendSubDft(unit, pids, blockParents, sparesAsLeaves);
- if(unit.empty()) {
+ if (unit.empty()) {
// Parent in the subdft, ie it is *not* a subdft
break;
}
@@ -84,26 +88,24 @@ namespace storm {
}
return std::vector<size_t>(unit.begin(), unit.end());
}
-
+
void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
- if(elemsInSubtree.count(this->id()) > 0) return;
+ if (elemsInSubtree.count(this->id()) > 0) 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;
}
if (!sparesAsLeaves) {
- for(auto const& child : this->mChildren) {
+ for (auto const& child : this->children()) {
child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
- if(elemsInSubtree.empty()) {
+ if (elemsInSubtree.empty()) {
// Parent in the subdft, ie it is *not* a subdft
return;
}
}
}
}
-
-
};
}
diff --git a/src/storm-dft/storage/dft/elements/DFTVot.h b/src/storm-dft/storage/dft/elements/DFTVot.h
index bb40998ac..920efb3e7 100644
--- a/src/storm-dft/storage/dft/elements/DFTVot.h
+++ b/src/storm-dft/storage/dft/elements/DFTVot.h
@@ -44,7 +44,7 @@ namespace storm {
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
if (state.isOperational(this->mId)) {
unsigned nrFailedChildren = 0;
- for (auto const& child : this->mChildren) {
+ for (auto const& child : this->children()) {
if (state.hasFailed(child->id())) {
++nrFailedChildren;
if (nrFailedChildren >= mThreshold) {
@@ -61,7 +61,7 @@ namespace storm {
STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child.");
if (state.isOperational(this->mId)) {
unsigned nrFailsafeChildren = 0;
- for (auto const& child : this->mChildren) {
+ for (auto const& child : this->children()) {
if (state.isFailsafe(child->id())) {
++nrFailsafeChildren;
if (nrFailsafeChildren > this->nrChildren() - mThreshold) {