From d0494d07e63ef3caaed86a4d003d40044576180d Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 3 Jun 2019 20:10:22 +0200
Subject: [PATCH] Get settings only once for takeFirstDependency

---
 .../generator/DftNextStateGenerator.cpp       | 10 ++++-----
 .../generator/DftNextStateGenerator.h         | 22 ++++++++++++++++---
 2 files changed, 24 insertions(+), 8 deletions(-)

diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index f4af34ed1..bbfe99dd6 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -12,6 +12,7 @@ namespace storm {
         template<typename ValueType, typename StateType>
         DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), uniqueFailedState(false) {
             deterministicModel = !mDft.canHaveNondeterminism();
+            mTakeFirstDependency = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isTakeFirstDependency();
         }
 
         template<typename ValueType, typename StateType>
@@ -48,11 +49,11 @@ namespace storm {
             STORM_LOG_DEBUG("Explore state: " << mDft.getStateString(state));
             // Initialization
             bool hasDependencies = state->getFailableElements().hasDependencies();
-            return exploreState(stateToIdCallback, hasDependencies);
+            return exploreState(stateToIdCallback, hasDependencies, mTakeFirstDependency);
         }
 
         template<typename ValueType, typename StateType>
-        StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies) {
+        StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies, bool takeFirstDependency) {
             // Prepare the result, in case we return early.
             StateBehavior<ValueType, StateType> result;
 
@@ -78,8 +79,7 @@ namespace storm {
             // Let BE fail
             bool isFirst = true;
             while (!state->getFailableElements().isEnd()) {
-                //TODO outside
-                if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isTakeFirstDependency() && exploreDependencies && !isFirst) {
+                if (takeFirstDependency && exploreDependencies && !isFirst) {
                     // We discard further exploration as we already chose one dependent event
                     break;
                 }
@@ -208,7 +208,7 @@ namespace storm {
                 if (result.empty()) {
                     // Dependencies might have been prevented from sequence enforcer
                     // -> explore BEs now
-                    return exploreState(stateToIdCallback, false);
+                    return exploreState(stateToIdCallback, false, takeFirstDependency);
                 }
             } else {
                 if (choice.size() == 0) {
diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h
index 9fab2ee1f..fc7580a13 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.h
+++ b/src/storm-dft/generator/DftNextStateGenerator.h
@@ -31,6 +31,12 @@ namespace storm {
 
             void load(storm::storage::BitVector const& state);
             void load(DFTStatePointer const& state);
+
+            /*!
+             * Expand and explore current state.
+             * @param stateToIdCallback  Callback function which adds new state and returns the corresponding id.
+             * @return  StateBehavior containing successor choices and distributions.
+             */
             StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback);
 
             /*!
@@ -44,7 +50,14 @@ namespace storm {
 
         private:
 
-            StateBehavior<ValueType, StateType> exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies);
+            /*!
+             * Explore current state and generate all successor states.
+             * @param stateToIdCallback Callback function which adds new state and returns the corresponding id.
+             * @param exploreDependencies Flag indicating whether failures due to dependencies or due to BEs should be explored.
+             * @param takeFirstDependency If true, instead of exploring all possible orders of dependency failures, a fixed order is explored where always the first dependency is considered.
+             * @return StateBehavior containing successor choices and distributions.
+             */
+            StateBehavior<ValueType, StateType> exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies, bool takeFirstDependency);
 
             // The dft used for the generation of next states.
             storm::storage::DFT<ValueType> const& mDft;
@@ -55,12 +68,15 @@ namespace storm {
             // Current state
             DFTStatePointer state;
 
-            // Flag indication if all failed states should be merged into one unique failed state.
+            // Flag indicating whether all failed states should be merged into one unique failed state.
             bool uniqueFailedState;
 
-            // Flag indicating if the model is deterministic.
+            // Flag indicating whether the model is deterministic.
             bool deterministicModel = false;
 
+            // Flag indicating whether only the first dependency (instead of all) should be explored.
+            bool mTakeFirstDependency = false;
+
         };
         
     }