From 8dfa141a4a02622e9c1d202813f8b2ff23e74561 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 24 May 2017 16:08:15 +0200
Subject: [PATCH] Exporting .dot for explicit input. removed duplicated code
 for explicit input with parametric engine

---
 src/storm/cli/cli.cpp       |  6 ++++++
 src/storm/cli/entrypoints.h | 36 ++++++++----------------------------
 src/storm/utility/storm.h   | 17 ++++++++++++++---
 3 files changed, 28 insertions(+), 31 deletions(-)

diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 7310f56c6..181a67480 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -322,6 +322,12 @@ namespace storm {
                     buildAndCheckExplicitModel<storm::RationalFunction>(properties, true);
 #else
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build.");
+#endif
+                } else if (generalSettings.isExactSet()) {
+#ifdef STORM_HAVE_CARL
+                    buildAndCheckExplicitModel<storm::RationalNumber>(properties, true);
+#else
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build.");
 #endif
                 } else {
                     buildAndCheckExplicitModel<double>(properties, true);
diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h
index b43db8bd9..5c04891eb 100644
--- a/src/storm/cli/entrypoints.h
+++ b/src/storm/cli/entrypoints.h
@@ -437,35 +437,15 @@ namespace storm {
                 STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model.");
                 verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), properties, onlyInitialStatesRelevant);
             }
-        }
-
-#ifdef STORM_HAVE_CARL
-        template<>
-        void buildAndCheckExplicitModel<storm::RationalFunction>(std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant) {
-            storm::settings::modules::IOSettings const& settings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-
-            STORM_LOG_THROW(settings.isExplicitSet() || settings.isExplicitDRNSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
-
-            storm::utility::Stopwatch modelBuildingWatch(true);
-            std::shared_ptr<storm::models::ModelBase> model;
-            STORM_LOG_THROW(!settings.isExplicitSet(), storm::exceptions::NotSupportedException, "Parametric explicit model files are not supported.");
-            model = buildExplicitDRNModel<storm::RationalFunction>(settings.getExplicitDRNFilename());
-            modelBuildingWatch.stop();
-            STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl);
-
-            // Preprocess the model if needed.
-            BRANCH_ON_MODELTYPE(model, model, storm::RationalFunction, storm::dd::DdType::CUDD, preprocessModel, extractFormulasFromProperties(properties));
-
-            // Print some information about the model.
-            model->printModelInformationToStream(std::cout);
-
-            // Verify the model, if a formula was given.
-            if (!properties.empty()) {
-                STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model.");
-                verifySparseModel<storm::RationalFunction>(model->as<storm::models::sparse::Model<storm::RationalFunction>>(), properties, onlyInitialStatesRelevant);
+            
+            // Export DOT if required.
+            if(storm::settings::getModule<storm::settings::modules::IOSettings>().isExportDotSet()) {
+                std::ofstream stream;
+                storm::utility::openFile(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportDotFilename(), stream);
+                model->as<storm::models::sparse::Model<ValueType>>()->writeDotToStream(stream);
+                storm::utility::closeFile(stream);
             }
-        }
-#endif
 
+        }
     }
 }
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index 0600c36d2..5c105b439 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -113,16 +113,27 @@ namespace storm {
         class FormulaParser;
     }
     
+    
     template<typename ValueType>
-    std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::none, boost::optional<std::string> const& transitionRewardsFile = boost::none, boost::optional<std::string> const& choiceLabelingFile = boost::none) {
-        return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
+    inline std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const&, std::string const&, boost::optional<std::string> const& = boost::none, boost::optional<std::string> const& = boost::none, boost::optional<std::string> const& = boost::none) {
+       STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact or parametric models with explicit input are not supported.");
     }
 
+    template<>
+    inline std::shared_ptr<storm::models::sparse::Model<double>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile, boost::optional<std::string> const& transitionRewardsFile, boost::optional<std::string> const& choiceLabelingFile) {
+        return storm::parser::AutoParser<double, double>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
+    }
+    
     template<typename ValueType>
-    std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitDRNModel(std::string const& drnFile) {
+    inline std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitDRNModel(std::string const& drnFile) {
         return storm::parser::DirectEncodingParser<ValueType>::parseModel(drnFile);
     }
 
+    template<>
+    inline std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> buildExplicitDRNModel(std::string const&) {
+       STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported.");
+    }
+
     std::vector<std::shared_ptr<storm::logic::Formula const>> extractFormulasFromProperties(std::vector<storm::jani::Property> const& properties);
     std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path);
     storm::prism::Program parseProgram(std::string const& path);