From 275a191b0840df847a8f40f4b361e028fde605e8 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 24 Nov 2017 10:17:41 +0100
Subject: [PATCH] Fixed spare claiming by adding missing constraint 'if the
 child is not claimed at the moment, it will never be claimed'.

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

diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index f112d2436..ae70b1317 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -465,6 +465,8 @@ namespace storm {
             uint64_t claimChild = getClaimVariableIndex(spare->id(), child->id()); // Moment the spare claims the child
 
             std::vector<std::shared_ptr<DFTConstraint>> noClaimingPossible;
+            // Child cannot be claimed.
+            noClaimingPossible.push_back(std::make_shared<IsEqual>(claimChild, notFailed));
             if (childIndex + 1 < spare->children().size()) {
                 // Consider next child for claiming (second case in constraint 7)
                 noClaimingPossible.push_back(generateTryToClaimConstraint(spare, childIndex+1, timepoint));