From d68829602253e6fb01f5ce6fcd7bbfd6bf68f195 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Tue, 15 Mar 2016 00:21:10 +0100
Subject: [PATCH] even more modularisation oppurtunaties are now taken

Former-commit-id: de8fd4c848df80c14380437fe6847eacab504d19
---
 src/modelchecker/DFTAnalyser.h | 5 ++---
 src/storage/dft/DFT.cpp        | 4 ++++
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/modelchecker/DFTAnalyser.h b/src/modelchecker/DFTAnalyser.h
index 0058f41f0..519b8090a 100644
--- a/src/modelchecker/DFTAnalyser.h
+++ b/src/modelchecker/DFTAnalyser.h
@@ -21,15 +21,14 @@ class DFTAnalyser {
     std::chrono::duration<double> totalTime = std::chrono::duration<double>::zero();
     ValueType checkResult = storm::utility::zero<ValueType>();
 public:
-    void check(storm::storage::DFT<ValueType> dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) {
+    void check(storm::storage::DFT<ValueType> const& origDft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) {
         
         // Building DFT
         std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
         
         
         // Optimizing DFT
-        dft = dft.optimize();
-        std::vector<storm::storage::DFT<ValueType>> dfts;
+        storm::storage::DFT<ValueType> dft = origDft.optimize();
         checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC);
         totalTime = std::chrono::high_resolution_clock::now() - totalStart;
             
diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index 4111a2113..b679b8a81 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -255,6 +255,7 @@ namespace storm {
             for(auto const& child : children) {
                 std::vector<size_t> isubdft;
                 if(child->nrParents() > 1 || child->hasOutgoingDependencies()) {
+                    STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
                     return {*this};
                 }
                 if (isGate(child->id())) {
@@ -262,7 +263,10 @@ namespace storm {
                 } else {
                     assert(isBasicElement(child->id()));
                     if(getBasicElement(child->id())->hasIngoingDependencies()) {
+                        STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
                         return {*this};
+                    } else {
+                        isubdft = {child->id()};
                     }
                     
                 }