diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp
index 0d145ef0c..12d85e000 100644
--- a/src/storm-dft/transformations/DftToGspnTransformator.cpp
+++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp
@@ -433,24 +433,48 @@ namespace storm {
                 double ycenter = mDft.getElementLayoutInfo(dftDependency->id()).y;;
                 
                 uint64_t coinPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_coin");
-                uint64_t flipPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_flip");
-                uint64_t forwardPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_forward");
+                builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter-5.0, ycenter+2.0));
                 uint64_t t1 = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_start_flip");
+                
                 builder.addInputArc(coinPlace, t1);
                 builder.addInputArc(failedNodes.at(dftDependency->triggerEvent()->id()), t1);
                 builder.addOutputArc(t1, failedNodes.at(dftDependency->triggerEvent()->id()));
-                builder.addOutputArc(t1, flipPlace);
-                uint64_t t2 = builder.addImmediateTransition(defaultPriority + 1, dftDependency->probability(), "_win_flip");
-                builder.addInputArc(flipPlace, t2);
-                builder.addOutputArc(t2, forwardPlace);
-                if (dftDependency->probability() < 1.0) {
-                    uint64_t t3 = builder.addImmediateTransition(defaultPriority + 1, 1 - dftDependency->probability(), "_loose_flip");
-                    builder.addInputArc(flipPlace, t3);
+                uint64_t forwardPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_forward");
+                builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter+1.0, ycenter+2.0));
+                
+                if (!smart || dftDependency->probability() < 1.0) {
+                    uint64_t flipPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_flip");
+                    builder.addOutputArc(t1, flipPlace);
+                    
+                    builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter-2.0, ycenter+2.0));
+                    uint64_t t2 = builder.addImmediateTransition(defaultPriority + 1, dftDependency->probability(), "_win_flip");
+                    builder.addInputArc(flipPlace, t2);
+                    builder.addOutputArc(t2, forwardPlace);
+                    if (dftDependency->probability() < 1.0) {
+                        uint64_t t3 = builder.addImmediateTransition(defaultPriority + 1, 1 - dftDependency->probability(), "_loose_flip");
+                        builder.addInputArc(flipPlace, t3);
+                    }
+                } else {
+                    builder.addOutputArc(t1, forwardPlace);
+                }
+                for(auto const& depEv : dftDependency->dependentEvents()) {
+                    uint64_t tx = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_propagate_" + depEv->name());
+                    builder.addInputArc(forwardPlace, tx);
+                    builder.addOutputArc(tx, forwardPlace);
+                    builder.addOutputArc(tx, failedNodes.at(depEv->id()));
+                    builder.addInhibitionArc(failedNodes.at(depEv->id()), tx);
+                    if (!smart || depEv->nrRestrictions() > 0) {
+                        builder.addInhibitionArc(disabledNodes.at(depEv->id()), tx);
+                    }
+                    if (!smart || mDft.isRepresentative(depEv->id())) {
+                        builder.addOutputArc(tx, unavailableNodes.at(depEv->id()));
+                    }
+                   
                 }
                 
-                builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter-5.0, ycenter+2.0));
-                builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter-2.0, ycenter+2.0));
-                builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter+1.0, ycenter+2.0));
+                
+                
+                
                 
 			}
             
@@ -536,59 +560,6 @@ namespace storm {
 			
 			template <typename ValueType>
             void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() {
-//				for (std::size_t i = 0; i < mDft.nrElements(); i++) {
-//					auto dftElement = mDft.getElement(i);
-//					
-//					if (dftElement->isRestriction()) {
-//						switch (dftElement->type()) {
-//							case storm::storage::DFTElementType::SEQ:
-//							{
-//								auto children = mDft.getRestriction(i)->children();
-//								
-//								for (std::size_t j = 0; j < children.size() - 1; j++) {
-//									auto suppressor = mGspn.getPlace(children[j]->name() + STR_FAILED);
-//									
-//									switch (children[j + 1]->type()) {
-//										case storm::storage::DFTElementType::BE: // If suppressed is a BE, add 2 arcs to timed transitions.
-//										{
-//											auto suppressedActive = mGspn.getTimedTransition(children[j + 1]->name() + "_activeFailing");
-//											auto suppressedPassive = mGspn.getTimedTransition(children[j + 1]->name() + "_passiveFailing");
-//											
-//											if (suppressor.first && suppressedActive.first && suppressedPassive.first) { // Only add arcs if the objects have been found.
-//												suppressedActive.second->setInputArcMultiplicity(suppressor.second, 1);
-//												suppressedActive.second->setOutputArcMultiplicity(suppressor.second, 1);
-//												suppressedPassive.second->setInputArcMultiplicity(suppressor.second, 1);
-//												suppressedPassive.second->setOutputArcMultiplicity(suppressor.second, 1);
-//											}
-//											break;
-//										}
-//										default: // If supressed is not a BE, add single arc to immediate transition.
-//										{
-//											auto suppressed = mGspn.getImmediateTransition(children[j + 1]->name() + STR_FAILING);
-//											
-//											if (suppressor.first && suppressed.first) { // Only add arcs if the objects have been found.
-//												suppressed.second->setInputArcMultiplicity(suppressor.second, 1);
-//												suppressed.second->setOutputArcMultiplicity(suppressor.second, 1);
-//											}
-//											break;
-//										}
-//									}
-//								}
-//								break;
-//							}
-//							case storm::storage::DFTElementType::MUTEX:
-//							{
-//								// MUTEX is not implemented by the DFTGalileoParser yet. Nothing to do here.
-//								STORM_LOG_ASSERT(false, "MUTEX is not supported by DftToGspnTransformator.");
-//								break;
-//							}
-//							default:
-//							{
-//								break;
-//							}
-//						}
-//					}
-//				}
 			}
 
 			template <typename ValueType>