From 003d2024c19f183dd5c530c758e68b8017c0f89b Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 22 Jan 2020 16:03:04 +0100
Subject: [PATCH] Restored functionality of --firstdep

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

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<ValueType, StateType> 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();