From d140da92cce10619e6bd6c501f630782af9fc032 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 17 Apr 2019 17:29:33 +0200
Subject: [PATCH] Small refactoring for ElementState

---
 src/storm-dft/storage/dft/DFT.cpp      |  6 ++----
 src/storm-dft/storage/dft/DFTState.cpp | 14 ++++++++++++--
 src/storm-dft/storage/dft/DFTState.h   | 12 ++++++++----
 3 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp
index 4a3a5eb30..7538c4abc 100644
--- a/src/storm-dft/storage/dft/DFT.cpp
+++ b/src/storm-dft/storage/dft/DFT.cpp
@@ -540,12 +540,10 @@ namespace storm {
             std::stringstream stream;
             stream << "(" << id << ") ";
             for (auto const& elem : mElements) {
-                size_t elemIndex = stateGenerationInfo.getStateIndex(elem->id());
-                int elementState = DFTState<ValueType>::getElementStateInt(status, elemIndex);
                 if (elem->isDependency()) {
-                    stream << storm::storage::toChar(static_cast<DFTDependencyState>(elementState)) << "[dep]";
+                    stream << storm::storage::toChar(DFTState<ValueType>::getDependencyState(status, stateGenerationInfo, elem->id())) << "[dep]";
                 } else {
-                    stream << storm::storage::toChar(static_cast<DFTElementState>(elementState));
+                    stream << storm::storage::toChar(DFTState<ValueType>::getElementState(status, stateGenerationInfo, elem->id()));
                     if(elem->isSpareGate()) {
                         stream << "[";
                         size_t nrUsedChild = status.getAsInt(stateGenerationInfo.getSpareUsageIndex(elem->id()), stateGenerationInfo.usageInfoBits());
diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp
index 778c571b8..689787b70 100644
--- a/src/storm-dft/storage/dft/DFTState.cpp
+++ b/src/storm-dft/storage/dft/DFTState.cpp
@@ -98,20 +98,30 @@ namespace storm {
         DFTElementState DFTState<ValueType>::getElementState(size_t id) const {
             return static_cast<DFTElementState>(getElementStateInt(id));
         }
+
+        template<typename ValueType>
+        DFTElementState DFTState<ValueType>::getElementState(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) {
+            return static_cast<DFTElementState>(DFTState<ValueType>::getElementStateInt(state, stateGenerationInfo, id));
+        }
         
         template<typename ValueType>
         DFTDependencyState DFTState<ValueType>::getDependencyState(size_t id) const {
             return static_cast<DFTDependencyState>(getElementStateInt(id));
         }
 
+        template<typename ValueType>
+        DFTDependencyState DFTState<ValueType>::getDependencyState(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) {
+            return static_cast<DFTDependencyState>(DFTState<ValueType>::getElementStateInt(state, stateGenerationInfo, id));
+        }
+
         template<typename ValueType>
         int DFTState<ValueType>::getElementStateInt(size_t id) const {
             return mStatus.getAsInt(mStateGenerationInfo.getStateIndex(id), 2);
         }
         
         template<typename ValueType>
-        int DFTState<ValueType>::getElementStateInt(storm::storage::BitVector const& state, size_t indexId) {
-            return state.getAsInt(indexId, 2);
+        int DFTState<ValueType>::getElementStateInt(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) {
+            return state.getAsInt(stateGenerationInfo.getStateIndex(id), 2);
         }
 
         template<typename ValueType>
diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h
index 97048fd2d..3718e7627 100644
--- a/src/storm-dft/storage/dft/DFTState.h
+++ b/src/storm-dft/storage/dft/DFTState.h
@@ -152,13 +152,13 @@ namespace storm {
             std::shared_ptr<DFTState<ValueType>> copy() const;
 
             DFTElementState getElementState(size_t id) const;
-            
+
+            static DFTElementState getElementState(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id);
+
             DFTDependencyState getDependencyState(size_t id) const;
 
-            int getElementStateInt(size_t id) const;
+            static DFTDependencyState getDependencyState(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id);
 
-            static int getElementStateInt(storm::storage::BitVector const& state, size_t indexId);
-            
             size_t getId() const;
 
             void setId(size_t id);
@@ -372,6 +372,10 @@ namespace storm {
         private:
             void propagateActivation(size_t representativeId);
 
+            int getElementStateInt(size_t id) const;
+
+            static int getElementStateInt(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id);
+
         };
 
     }