diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index ccfa5bdf4..4a4432f78 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -376,18 +376,21 @@ namespace storm { template void DftToGspnTransformator::drawSeq(std::shared_ptr const> dftSeq) { STORM_LOG_THROW(dftSeq->allChildrenBEs(), storm::exceptions::NotImplementedException, "Sequence enforcers with gates as children are currently not supported"); - bool first = true; + uint64_t j = 0; uint64_t tEnable = 0; uint64_t nextPlace = 0; for(auto const& child : dftSeq->children()) { - nextPlace = builder.addPlace(defaultCapacity, first ? 1 : 0, dftSeq->name() + "_next_" + child->name()); - if(!first) { + nextPlace = builder.addPlace(defaultCapacity, j==0 ? 1 : 0, dftSeq->name() + "_next_" + child->name()); + if (j>0) { builder.addOutputArc(tEnable, nextPlace); } tEnable = builder.addImmediateTransition(defaultPriority, 0.0, dftSeq->name() + "_unblock_" +child->name() ); builder.addInputArc(nextPlace, tEnable); builder.addInputArc(disabledNodes.at(child->id()), tEnable); - first = false; + if (j>0) { + builder.addInputArc(failedNodes.at(dftSeq->children().at(j-1)->id()), tEnable); + } + ++j; } }