From bf88eca92f6c33c0fe3aea26d95abb9e77978c47 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 10 Apr 2018 15:25:45 +0200
Subject: [PATCH] Export DRN format for model composed from DFT modularisation

---
 src/storm-dft/modelchecker/dft/DFTModelChecker.cpp | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 8d277d60d..997113bd2 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -28,6 +28,18 @@ namespace storm {
             if (properties[0]->isTimeOperatorFormula() && allowModularisation) {
                 // Use parallel composition as modularisation approach for expected time
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, enableDC, approximationError);
+
+                // Export the model if required
+                // TODO move this outside of the model checker?
+                if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet()) {
+                    std::ofstream stream;
+                    storm::utility::openFile(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportExplicitFilename(), stream);
+                    std::vector<std::string> parameterNames;
+                    // TODO fill parameter names
+                    storm::exporter::explicitExportSparseModel(stream, model, parameterNames);
+                    storm::utility::closeFile(stream);
+                }
+
                 // Model checking
                 std::vector<ValueType> resultsValue = checkModel(model, properties);
                 for (ValueType result : resultsValue) {