From fac77c0a3eac62f4a6873733de2b1468af3964c9 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 14 Dec 2016 23:14:54 +0100
Subject: [PATCH] fixed seq, now correct...

---
 .../transformations/DftToGspnTransformator.cpp        | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

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 <typename ValueType>
             void DftToGspnTransformator<ValueType>::drawSeq(std::shared_ptr<storm::storage::DFTSeq<ValueType> 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;
                 }
                 
             }