diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 29dc71238..0844f08f9 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -120,8 +120,14 @@ namespace storm { Choice choice(0, !exploreDependencies); // Let BE fail + bool isFirst = true; while (!state->getFailableElements().isEnd()) { //TODO outside + if (takeFirstDependency && exploreDependencies && !isFirst) { + // We discard further exploration as we already chose one dependent event + break; + } + isFirst = false; // Construct new state as copy from original one DFTStatePointer newState = state->copy();