From 868c9fb0fd113ad39612aa615d2f26d880665cf0 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 5 Feb 2021 14:05:36 +0100
Subject: [PATCH] Fixed activation for failed nested SPAREs.

If a nested (passive) SPARE is already failed and it becomes activated (through claiming), it will not activate its children.
---
 src/storm-dft/storage/dft/DFTState.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp
index 6c58b0923..abfcdad58 100644
--- a/src/storm-dft/storage/dft/DFTState.cpp
+++ b/src/storm-dft/storage/dft/DFTState.cpp
@@ -387,8 +387,13 @@ namespace storm {
                                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BE type '" << be->type() << "' is not supported.");
                         }
                     }
-                } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {
-                    propagateActivation(uses(elem));
+                } else if (mDft.getElement(elem)->isSpareGate()){
+                    if (isOperational(elem)) {
+                        // We do not activate children if the SPARE is already failed
+                        if (!isActive(uses(elem))) {
+                            propagateActivation(uses(elem));
+                        }
+                    }
                 }
             }
         }