From d1b86c8f355826176c94a34c9584e6f0e2ed6982 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 9 Feb 2017 00:24:35 +0100
Subject: [PATCH] Failed states are Markovian

---
 src/storm-dft/generator/DftNextStateGenerator.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index 3f1361f93..c89368099 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -52,10 +52,10 @@ namespace storm {
             bool hasDependencies = state->nrFailableDependencies() > 0;
             size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
             size_t currentFailable = 0;
-            Choice<ValueType, StateType> choice(0, !hasDependencies);
 
             // Check for absorbing state
             if (mDft.hasFailed(state) || mDft.isFailsafe(state) || failableCount == 0) {
+                Choice<ValueType, StateType> choice(0, true);
                 // Add self loop
                 choice.addProbability(state->getId(), storm::utility::one<ValueType>());
                 STORM_LOG_TRACE("Added self loop for " << state->getId());
@@ -65,6 +65,8 @@ namespace storm {
                 return result;
             }
 
+            Choice<ValueType, StateType> choice(0, !hasDependencies);
+
             // Let BE fail
             while (currentFailable < failableCount) {
                 STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed.");