From d04268a29430b560db20ceb9f592d06362b7e322 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Sun, 24 Jan 2021 22:18:21 +0100
Subject: [PATCH] Added const qualifiers

---
 .../generator/DftNextStateGenerator.cpp       | 21 ++++++++++++-------
 .../generator/DftNextStateGenerator.h         | 13 +++++++++---
 2 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index 7d4894284..10f01fbe2 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -20,9 +20,16 @@ namespace storm {
             return deterministicModel;
         }
 
+        template<typename ValueType, typename StateType>
+        typename DftNextStateGenerator<ValueType, StateType>::DFTStatePointer DftNextStateGenerator<ValueType, StateType>::createInitialState() const {
+            return std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
+        }
+
         template<typename ValueType, typename StateType>
         std::vector<StateType> DftNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
-            DFTStatePointer initialState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
+            DFTStatePointer initialState = createInitialState();
+
+            // Check whether constant failed BEs are present
             size_t constFailedBeCounter = 0;
             std::shared_ptr<storm::storage::DFTBE<ValueType> const> constFailedBE = nullptr;
             for (auto &be : mDft.getBasicElements()) {
@@ -214,7 +221,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        typename DftNextStateGenerator<ValueType, StateType>::DFTStatePointer DftNextStateGenerator<ValueType, StateType>::createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const>& failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>& triggeringDependency) {
+        typename DftNextStateGenerator<ValueType, StateType>::DFTStatePointer DftNextStateGenerator<ValueType, StateType>::createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const>& failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>& triggeringDependency) const {
             // Construct new state as copy from original one
             DFTStatePointer newState = state->copy();
             STORM_LOG_TRACE("With the failure of: " << failedBE->name() << " [" << failedBE->id() << "]" << (triggeringDependency != nullptr ? " (through dependency " + triggeringDependency->name() + " [" + std::to_string(triggeringDependency->id()) + ")]" : "") << " in " << mDft.getStateString(state));
@@ -254,9 +261,8 @@ namespace storm {
 
 
         template<typename ValueType, typename StateType>
-        void DftNextStateGenerator<ValueType, StateType>::propagateFailure(DFTStatePointer newState,
-                                                                           std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
-                                                                           storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) {
+        void DftNextStateGenerator<ValueType, StateType>::propagateFailure(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
+                                                                           storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) const {
             // Propagate failure
             for (DFTGatePointer parent : nextBE->parents()) {
                 if (newState->isOperational(parent->id())) {
@@ -285,9 +291,8 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void DftNextStateGenerator<ValueType, StateType>::propagateFailsafe(DFTStatePointer newState,
-                                                                            std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
-                                                                            storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) {
+        void DftNextStateGenerator<ValueType, StateType>::propagateFailsafe(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
+                                                                            storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) const {
             // Propagate failsafe
             while (!queues.failsafePropagationDone()) {
                 DFTGatePointer next = queues.nextFailsafePropagation();
diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h
index afac7041f..af13b4750 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.h
+++ b/src/storm-dft/generator/DftNextStateGenerator.h
@@ -48,6 +48,13 @@ namespace storm {
              */
             StateBehavior<ValueType, StateType> createMergeFailedState(StateToIdCallback const& stateToIdCallback);
 
+            /*!
+             * Create initial state.
+             * 
+             * @return Initial state.
+             */
+            DFTStatePointer createInitialState() const;
+
             /*!
              * Create successor state from given state by letting the given BE fail next.
              * 
@@ -57,7 +64,7 @@ namespace storm {
              * 
              * @return Successor state.
              */
-            DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const> &triggeringDependency);
+            DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const> &triggeringDependency) const;
 
             /**
              * Propagate the failures in a given state if the given BE fails
@@ -67,7 +74,7 @@ namespace storm {
              */
             void
             propagateFailure(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
-                             storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues);
+                             storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) const;
 
             /**
              * Propagate the failsafe state in a given state if the given BE fails
@@ -77,7 +84,7 @@ namespace storm {
              */
             void
             propagateFailsafe(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
-                              storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues);
+                              storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) const;
 
         private: