Merge branch 'monolithic-dft-update' of https://sselab.de/lab9/private/git/storm into monolithic-dft-update

Former-commit-id: a4d88f2026

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;
             

src/storage/dft/DFT.cpp

@@ -250,6 +250,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())) {
@@ -257,7 +258,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()};
                     }
                     
                 }