diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 4e9808835..a200563b1 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -32,8 +32,11 @@ namespace storm { auto wellFormedResult = storm::api::isWellFormed(origDft, true); STORM_LOG_THROW(wellFormedResult.first, storm::exceptions::UnmetRequirementException, "DFT is not well-formed for analysis: " << wellFormedResult.second); - // Optimizing DFT - storm::storage::DFT dft = origDft.optimize(); + // Optimizing DFT for modularisation + storm::storage::DFT dft = origDft; + if (allowModularisation) { + dft = origDft.optimize(); + } // TODO: check that all paths reach the target state for approximation