diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index f04aa79c8..c95a7f21d 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/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); } + }