From 20b00e8f1dcff6e72df2c6011b5b4622f7046870 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 25 Oct 2016 00:25:35 +0200
Subject: [PATCH] Propagate dont care to currently not failable BEs

Former-commit-id: 1fcb15f4ec045d244e1397b4fbe2100435ea9557
---
 src/storage/dft/DFTState.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index 0b2ff7ee8..369bed3f7 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -200,8 +200,13 @@ namespace storm {
         template<typename ValueType>
         void DFTState<ValueType>::beNoLongerFailable(size_t id) {
             auto it = std::find(mCurrentlyFailableBE.begin(), mCurrentlyFailableBE.end(), id);
-            if(it != mCurrentlyFailableBE.end()) {
+            if (it != mCurrentlyFailableBE.end()) {
                 mCurrentlyFailableBE.erase(it);
+            } else {
+                it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), id);
+                if (it != mCurrentlyNotFailableBE.end()) {
+                    mCurrentlyNotFailableBE.erase(it);
+                }
             }
         }
 
@@ -253,7 +258,7 @@ namespace storm {
         ValueType DFTState<ValueType>::getNotFailableBERate(size_t index) const {
             STORM_LOG_ASSERT(index < nrNotFailableBEs(), "Index invalid.");
             STORM_LOG_ASSERT(storm::utility::isZero<ValueType>(mDft.getBasicElement(mCurrentlyNotFailableBE[index])->activeFailureRate()) ||
-                             (mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail");
+                             (mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail in state: " << mDft.getStateString(mStatus, mStateGenerationInfo, mId));
             // Use active failure rate as passive failure rate is 0.
             return getBERate(mCurrentlyNotFailableBE[index], false);
         }