From 3987458ed84b94ddc7399928a761683314fa6198 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 24 Nov 2017 20:00:45 +0100
Subject: [PATCH] Fixed bug in claiming by only considering spare parents

---
 src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index 60f6976d6..06bfd1cca 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -566,10 +566,10 @@ namespace storm {
                         // Child must be operational at time of claiming
                         additionalC.push_back(std::make_shared<IsLess>(timeClaiming, timePointVariables.at(child->id())));
                         // No other spare claims this child
-                        for (auto const& otherSpare : child->parents()) {
-                            if (otherSpare->id() != spare->id()) {
+                        for (auto const& parent : child->parents()) {
+                            if (parent->isSpareGate() && parent->id() != spare->id()) {
                                 // Different spare
-                                additionalC.push_back(std::make_shared<IsConstantValue>(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed));
+                                additionalC.push_back(std::make_shared<IsConstantValue>(getClaimVariableIndex(parent->id(), child->id()), notFailed));
                             }
                         }
                         constraints.push_back(std::make_shared<Implies>(leftC, std::make_shared<And>(additionalC)));