Merge

src/storm-dft/transformations/DftToGspnTransformator.cpp

@@ -384,7 +384,7 @@ namespace storm {
                 if (isRepresentative) {
                     unavailableNode = addUnavailableNode(dftSpare, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0));
                 }
-                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);
                 builder.setPlaceLayoutInfo(spareActive, storm::gspn::LayoutInfo(xcenter-20.0, ycenter-8.0));
                 activeNodes.emplace(dftSpare->id(), spareActive);
 
@@ -430,6 +430,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);
@@ -439,6 +449,7 @@ namespace storm {
                     builder.addOutputArc(nextclTransitions.back(), unavailableNode);
                 }
                 
+                
 
 			}