From 2c15c897510daa9a517d7a8839a0b3f6326d1256 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Mon, 14 Mar 2016 23:15:07 +0100
Subject: [PATCH] No DC propagation for failed toplevel

Former-commit-id: a2cf30e0718699411e8972f2c2b8bbb3de6b9455
---
 src/builder/ExplicitDFTModelBuilder.cpp | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index f5296a487..09fde00ef 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -212,21 +212,23 @@ namespace storm {
                     if(newState->isInvalid()) {
                         continue;
                     }
-
-                    while (!queues.failsafePropagationDone()) {
+                    bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex());
+                    
+                    while (!dftFailed && !queues.failsafePropagationDone()) {
                         DFTGatePointer next = queues.nextFailsafePropagation();
                         next->checkFailsafe(*newState, queues);
                     }
 
-                    while (enableDC && !queues.dontCarePropagationDone()) {
+                    while (!dftFailed && enableDC && !queues.dontCarePropagationDone()) {
                         DFTElementPointer next = queues.nextDontCarePropagation();
                         next->checkDontCareAnymore(*newState, queues);
                     }
                     
                     // Update failable dependencies
-                    newState->updateFailableDependencies(nextBE->id());
+                    if (!dftFailed) {
+                        newState->updateFailableDependencies(nextBE->id());
+                    }
                     
-                    bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex());
                     uint_fast64_t newStateId;
                     if(dftFailed && mergeFailedStates) {
                         newStateId = failedIndex;