From 2e8460548b9110a439a519b4e0facbdeb520a5d6 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 23 Feb 2016 13:52:48 +0100
Subject: [PATCH] Failed spares set use index to own id

Former-commit-id: e4da5bd5d8d0400fed1531b2891422a918dc090c
---
 src/storage/dft/DFT.cpp       | 10 +++++-----
 src/storage/dft/DFTElements.h |  4 ++--
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index b61425953..eef83928d 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -263,10 +263,10 @@ namespace storm {
                     stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id()));
                     if(elem->isSpareGate()) {
                         size_t useId = state->uses(elem->id());
-                        if(state->isActive(useId)) {
-                            stream << " actively ";
+                        if(useId == elem->id() || state->isActive(useId)) {
+                            stream << "actively ";
                         }
-                        stream << " using " << useId;
+                        stream << "using " << useId;
                     }
                 }
                 stream << std::endl;
@@ -287,8 +287,8 @@ namespace storm {
                     if(elem->isSpareGate()) {
                         stream << "[";
                         size_t useId = state->uses(elem->id());
-                        if(state->isActive(useId)) {
-                            stream << " actively ";
+                        if(useId == elem->id() || state->isActive(useId)) {
+                            stream << "actively ";
                         }
                         stream << "using " << useId << "]";
                     }
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index bb4be80a7..3236a5551 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -412,12 +412,12 @@ namespace storm {
             }
 
             /**
-             * Finish failed/failsafe spare gate by activating the children and setting the useIndex to zero.
+             * Finish failed/failsafe spare gate by activating the children and setting the useIndex to the spare id.
              * This prevents multiple fail states with different usages or activations.
              * @param state The current state.
              */
             void finalizeSpare(DFTState<ValueType>& state) const {
-                state.setUses(this->mId, 0);
+                state.setUses(this->mId, this->mId);
                 for (auto child : this->children()) {
                     if (!state.isActive(child->id())) {
                         state.activate(child->id());