From 94cd2e7fbd8be2f846dee8c8c8f900e831c88c1a Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 17 Feb 2021 12:52:02 +0100
Subject: [PATCH] Apply rewriting only for modularisation

---
 src/storm-dft/modelchecker/dft/DFTModelChecker.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

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<ValueType> dft = origDft.optimize();
+            // Optimizing DFT for modularisation
+            storm::storage::DFT<ValueType> dft = origDft;
+            if (allowModularisation) {
+                dft = origDft.optimize();
+            }
 
             // TODO: check that all paths reach the target state for approximation