From d31fae859f5377e6becc97d620965810644814a4 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Tue, 26 Feb 2019 21:26:04 +0100
Subject: [PATCH] Added error handling of gates with restricton as child and
 changed order of topoSort and rank computation to ensure that rank is only
 computed for acyclic DFTs

---
 src/storm-dft/builder/DFTBuilder.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp
index 87bd5f407..54eb06779 100644
--- a/src/storm-dft/builder/DFTBuilder.cpp
+++ b/src/storm-dft/builder/DFTBuilder.cpp
@@ -26,6 +26,9 @@ namespace storm {
                     if (itFind != mElements.end()) {
                         // Child found
                         DFTElementPointer childElement = itFind->second;
+                        STORM_LOG_THROW(!childElement->isRestriction(), storm::exceptions::WrongFormatException,
+                                        "Restictor " << childElement->name() << " is not allowed as child of gate "
+                                                     << gate->name());
                         if(!childElement->isDependency()) {
                             gate->pushBackChild(childElement);
                             childElement->addParent(gate);
@@ -82,14 +85,13 @@ namespace storm {
                 }
                 
             }
-            
 
             // Sort elements topologically
+            DFTElementVector elems = topoSort();
             // compute rank
-            for (auto& elem : mElements) {
+            for (auto &elem : mElements) {
                 computeRank(elem.second);
             }
-            DFTElementVector elems = topoSort();
             // Set ids
             size_t id = 0;
             for(DFTElementPointer e : elems) {