From 365b7e7673e2f19f66d7a531bba36a995b3b119e Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 4 Apr 2019 11:21:24 +0200
Subject: [PATCH] Removed mChildren in DFTRestriction

---
 .../storage/dft/elements/DFTChildren.h        |  5 +++++
 src/storm-dft/storage/dft/elements/DFTGate.h  |  4 ++--
 .../storage/dft/elements/DFTRestriction.h     | 20 +++++++++----------
 3 files changed, 16 insertions(+), 13 deletions(-)

diff --git a/src/storm-dft/storage/dft/elements/DFTChildren.h b/src/storm-dft/storage/dft/elements/DFTChildren.h
index 5a0e53776..a9d0c7290 100644
--- a/src/storm-dft/storage/dft/elements/DFTChildren.h
+++ b/src/storm-dft/storage/dft/elements/DFTChildren.h
@@ -158,6 +158,11 @@ namespace storm {
                 return false;
             }
 
+            virtual void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
+
+            virtual void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
+
+
         private:
             DFTElementVector mChildren;
 
diff --git a/src/storm-dft/storage/dft/elements/DFTGate.h b/src/storm-dft/storage/dft/elements/DFTGate.h
index 1c3000c85..9f95ed751 100644
--- a/src/storm-dft/storage/dft/elements/DFTGate.h
+++ b/src/storm-dft/storage/dft/elements/DFTGate.h
@@ -67,7 +67,7 @@ namespace storm {
 
         protected:
 
-            virtual void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+            void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 for (std::shared_ptr<DFTGate> parent : this->mParents) {
                     if (state.isOperational(parent->id())) {
                         queues.propagateFailure(parent);
@@ -80,7 +80,7 @@ namespace storm {
                 this->childrenDontCare(state, queues);
             }
 
-            virtual void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+            void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 for (std::shared_ptr<DFTGate> parent : this->mParents) {
                     if (state.isOperational(parent->id())) {
                         queues.propagateFailsafe(parent);
diff --git a/src/storm-dft/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h
index d1a69c98b..9b93ae63a 100644
--- a/src/storm-dft/storage/dft/elements/DFTRestriction.h
+++ b/src/storm-dft/storage/dft/elements/DFTRestriction.h
@@ -49,7 +49,7 @@ namespace storm {
              * @return True iff all children are BEs.
              */
             bool allChildrenBEs() const {
-                for (auto const& elem : mChildren) {
+                for (auto const& elem : this->children()) {
                     if (!elem->isBasicElement()) {
                         return false;
                     }
@@ -57,25 +57,23 @@ namespace storm {
                 return true;
             }
 
-            virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
+            void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
                 // Do nothing
             }
 
-            virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
+            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
                 return false;
             }
 
 
         protected:
-            void fail(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const {
+            void fail(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
                 state.markAsInvalid();
             }
 
-            void failsafe(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const {
+            void failsafe(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
 
             }
-
-            DFTElementVector mChildren;
         };
 
 
@@ -98,18 +96,18 @@ namespace storm {
                 // Intentionally left empty.
             }
 
-            virtual DFTElementType type() const override {
+            DFTElementType type() const override {
                 return DFTElementType::SEQ;
             }
 
-            virtual bool isSeqEnforcer() const override {
+            bool isSeqEnforcer() const override {
                 return true;
             }
 
             void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
                 STORM_LOG_ASSERT(queues.failurePropagationDone(), "Failure propagation not finished.");
                 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())) {
@@ -122,7 +120,7 @@ namespace storm {
             void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
             }
 
-            virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
+            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
                 // Actually, it doesnt matter what we return here..
                 return false;
             }