From 146bd193ea370484d134b1f1a16918f5137ea810 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 15 Dec 2016 12:03:00 +0100
Subject: [PATCH] spare activation

---
 .../transformations/DftToGspnTransformator.cpp    | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp
index 12d85e000..f97faa404 100644
--- a/src/storm-dft/transformations/DftToGspnTransformator.cpp
+++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp
@@ -280,7 +280,7 @@ namespace storm {
                             builder.addInhibitionArc(failedNodes.at(child->id()), tn);
                         }
                         if (j != dftPand->nrChildren() - 1) {
-                            tn = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(j));
+                            tn = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" + std::to_string(j));
                         } else {
                             tn = tNodeFailed;
                         }
@@ -307,7 +307,7 @@ namespace storm {
                 if (isRepresentative) {
                     unavailableNode = addUnavailableNode(dftSpare);
                 }
-                uint64_t spareActive = builder.addPlace(defaultCapacity, 0, dftSpare->name() + STR_ACTIVATED);
+                uint64_t spareActive = builder.addPlace(defaultCapacity, isBEActive(dftSpare) ? 1 : 0, dftSpare->name() + STR_ACTIVATED);
                 activeNodes.emplace(dftSpare->id(), spareActive);
 
                 
@@ -345,6 +345,16 @@ namespace storm {
                     builder.addOutputArc(tnextcl, failedNodes.at(child->id()));
                     nextclTransitions.push_back(tnextcl);
                     ++j;
+                    for (uint64_t k : mDft.module(child->id())) {
+                        
+                        uint64_t tactive = builder.addImmediateTransition(defaultPriority+1, 0.0, dftSpare->name() + "_activate_" + std::to_string(j) + "_" +  std::to_string(k));
+                        builder.addInputArc(cucNodes.back(), tactive);
+                        builder.addInputArc(spareActive, tactive);
+                        builder.addOutputArc(tactive, activeNodes.at(k));
+                        builder.addInhibitionArc(activeNodes.at(k), tactive);
+                    }
+                    
+                    
                 }
                 builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed);
                 builder.addOutputArc(nextclTransitions.back(), nodeFailed);
@@ -354,6 +364,7 @@ namespace storm {
                     builder.addOutputArc(nextclTransitions.back(), unavailableNode);
                 }
                 
+                
 
 			}
 //