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 totalTime = std::chrono::duration::zero(); ValueType checkResult = storm::utility::zero(); public: - void check(storm::storage::DFT dft , std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) { + void check(storm::storage::DFT const& origDft , std::shared_ptr 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> dfts; + storm::storage::DFT 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 653a5dc78..9a1b086fc 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -250,6 +250,7 @@ namespace storm { for(auto const& child : children) { std::vector 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()}; } }