From 32dc2dbcc0954232404b2240119f6dd73973c5bb Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 22 Apr 2019 23:18:44 +0200
Subject: [PATCH] Fixed bug where children of SEQ gates were not properly
 enabled

---
 src/storm-dft/storage/dft/DFTState.cpp | 29 +++++++++++++-------------
 1 file changed, 14 insertions(+), 15 deletions(-)

diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp
index 689787b70..c62f290f3 100644
--- a/src/storm-dft/storage/dft/DFTState.cpp
+++ b/src/storm-dft/storage/dft/DFTState.cpp
@@ -259,23 +259,22 @@ namespace storm {
                 STORM_LOG_ASSERT(restriction->containsChild(id), "Ids do not match.");
                 if (restriction->isSeqEnforcer()) {
                     for (auto it = restriction->children().cbegin(); it != restriction->children().cend(); ++it) {
-                        if ((*it)->isBasicElement()) {
-                            if ((*it)->id() != id) {
-                                if (!hasFailed((*it)->id())) {
-                                    // Failure should be prevented later on
-                                    STORM_LOG_TRACE("Child " << (*it)->id() << " should have failed.");
-                                }
-                            } else {
-                                // Current event has failed
-                                ++it;
-                                if (it != restriction->children().cend()) {
-                                    // Enable next event
-                                    failableElements.addBE((*it)->id());
-                                    STORM_LOG_TRACE("Added possible BE failure: " << *(*it));
-                                    addedFailableEvent = true;
-                                }
+                        if ((*it)->id() != id) {
+                            if (!hasFailed((*it)->id())) {
+                                // Failure should be prevented later on
+                                STORM_LOG_TRACE("Child " << (*it)->name() << " should have failed.");
                                 break;
                             }
+                        } else {
+                            // Current event has failed
+                            ++it;
+                            if (it != restriction->children().cend() && (*it)->isBasicElement()) {
+                                // Enable next event
+                                failableElements.addBE((*it)->id());
+                                STORM_LOG_TRACE("Added possible BE failure: " << *(*it));
+                                addedFailableEvent = true;
+                            }
+                            break;
                         }
                     }
                 } else if (restriction->isMutex()) {