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 choice(0, !hasDependencies); // Check for absorbing state if (mDft.hasFailed(state) || mDft.isFailsafe(state) || failableCount == 0) { + Choice choice(0, true); // Add self loop choice.addProbability(state->getId(), storm::utility::one()); STORM_LOG_TRACE("Added self loop for " << state->getId()); @@ -65,6 +65,8 @@ namespace storm { return result; } + Choice choice(0, !hasDependencies); + // Let BE fail while (currentFailable < failableCount) { STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed.");