From 9656d2c253f01fcc157960c714456d06e10b5135 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 14 Nov 2018 18:11:57 +0100
Subject: [PATCH] Supporting export of generated Markov chain from DFT

---
 .../modelchecker/dft/DFTModelChecker.cpp          | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 2a2a62e14..35367ed3a 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -342,23 +342,24 @@ namespace storm {
                 return results;
             } else {
                 // Build a single Markov Automaton
+                auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
                 STORM_LOG_DEBUG("Building Model...");
                 storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
-                typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
+                typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, ioSettings.isExportExplicitSet() || ioSettings.isExportDotSet());
                 builder.buildModel(labeloptions, 0, 0.0);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
-                //model->printModelInformationToStream(std::cout);
+                model->printModelInformationToStream(std::cout);
                 explorationTimer.stop();
 
                 // 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);
+                if (ioSettings.isExportExplicitSet()) {
                     std::vector<std::string> parameterNames;
                     // TODO fill parameter names
-                    storm::exporter::explicitExportSparseModel(stream, model, parameterNames);
-                    storm::utility::closeFile(stream);
+                    storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), parameterNames);
+                }
+                if (ioSettings.isExportDotSet()) {
+                    storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename());
                 }
 
                 // Model checking