From 21c970f8f75a4f61abc50602fcdca6ab36a55123 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 2 Apr 2018 13:02:17 +0200
Subject: [PATCH] added dd-to-sparse engine that builds the model as a DD and
 then transforms the whole model to a sparse representation

---
 src/storm-cli-utilities/model-handling.h    | 21 ++++++++++++++++++++-
 src/storm/settings/modules/CoreSettings.cpp |  4 +++-
 src/storm/settings/modules/CoreSettings.h   |  2 +-
 3 files changed, 24 insertions(+), 3 deletions(-)

diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index c279dc742..35390c7cb 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -217,7 +217,7 @@ namespace storm {
             auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             std::shared_ptr<storm::models::ModelBase> result;
             if (input.model) {
-                if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
+                if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::DdSparse || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
                     result = buildModelDd<DdType, ValueType>(input);
                 } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
                     result = buildModelSparse<ValueType>(input, buildSettings);
@@ -350,6 +350,25 @@ namespace storm {
                 result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(symbolicModel->template toValueType<ExportValueType>(), !std::is_same<ValueType, ExportValueType>::value);
             }
             
+            if (result && result->first->isSymbolicModel() && storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::DdSparse) {
+                // Mark as changed.
+                result->second = true;
+                
+                std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> symbolicModel = result->first->template as<storm::models::symbolic::Model<DdType, ExportValueType>>();
+                if (symbolicModel->isOfType(storm::models::ModelType::Dtmc)) {
+                    storm::transformer::SymbolicDtmcToSparseDtmcTransformer<DdType, ExportValueType> transformer;
+                    result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<DdType, ExportValueType>>());
+                } else if (symbolicModel->isOfType(storm::models::ModelType::Ctmc)) {
+                    storm::transformer::SymbolicCtmcToSparseCtmcTransformer<DdType, ExportValueType> transformer;
+                    result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<DdType, ExportValueType>>());
+                } else if (symbolicModel->isOfType(storm::models::ModelType::Mdp)) {
+                    storm::transformer::SymbolicMdpToSparseMdpTransformer<DdType, ExportValueType> transformer;
+                    result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Mdp<DdType, ExportValueType>>());
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The translation to a sparse model is not supported for the given model type.");
+                }
+            }
+            
             return *result;
         }
         
diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp
index 9bcd4d77c..8419f209f 100644
--- a/src/storm/settings/modules/CoreSettings.cpp
+++ b/src/storm/settings/modules/CoreSettings.cpp
@@ -39,7 +39,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model.").setShortName(counterexampleOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build());
                 
-                std::vector<std::string> engines = {"sparse", "hybrid", "dd", "expl", "abs"};
+                std::vector<std::string> engines = {"sparse", "hybrid", "dd", "dd-to-sparse", "expl", "abs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("sparse").build()).build());
                 
@@ -164,6 +164,8 @@ namespace storm {
                     engine = CoreSettings::Engine::Hybrid;
                 } else if (engineStr == "dd") {
                     engine = CoreSettings::Engine::Dd;
+                } else if (engineStr == "dd-to-sparse") {
+                    engine = CoreSettings::Engine::DdSparse;
                 } else if (engineStr == "expl") {
                     engine = CoreSettings::Engine::Exploration;
                 } else if (engineStr == "abs") {
diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h
index afd16cd78..8a07a48d0 100644
--- a/src/storm/settings/modules/CoreSettings.h
+++ b/src/storm/settings/modules/CoreSettings.h
@@ -28,7 +28,7 @@ namespace storm {
             public:
                 // An enumeration of all engines.
                 enum class Engine {
-                    Sparse, Hybrid, Dd, Exploration, AbstractionRefinement
+                    Sparse, Hybrid, Dd, DdSparse, Exploration, AbstractionRefinement
                 };
 
                 /*!