From 367b8f0a3e6b287c5ddbcb27a65a3dfd068cd1fc Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 7 Apr 2017 17:07:26 +0200
Subject: [PATCH] parameter lifting with hybrid engine

---
 src/storm/cli/entrypoints.h                   | 12 ++++++++-
 .../SymbolicToSparseTransformer.cpp           | 27 +++++++++++++++++--
 .../transformer/SymbolicToSparseTransformer.h |  3 +++
 src/storm/utility/storm.h                     |  1 +
 4 files changed, 40 insertions(+), 3 deletions(-)

diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h
index e7e826cd1..723f9b5df 100644
--- a/src/storm/cli/entrypoints.h
+++ b/src/storm/cli/entrypoints.h
@@ -290,7 +290,17 @@ namespace storm {
             
             // Then select the correct engine.
             if (hybrid) {
-                verifySymbolicModelWithHybridEngine<LibraryType, ValueType>(markovModel, properties, onlyInitialStatesRelevant);
+                if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isParameterLiftingSet()) {
+                    STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet(), storm::exceptions::InvalidSettingsException, "Invoked parameter lifting without enabling the parametric engine.");
+                    STORM_PRINT_AND_LOG("Transforming symbolic model to sparse model ...");
+                    auto sparseModel = storm::transformer::transformSymbolicToSparseModel(markovModel);
+                    STORM_PRINT_AND_LOG(" done" << std::endl);
+                    sparseModel->printModelInformationToStream(std::cout);
+                    auto formulas = extractFormulasFromProperties(properties);
+                    storm::performParameterLifting<ValueType>(sparseModel, formulas);
+                } else {
+                    verifySymbolicModelWithHybridEngine<LibraryType, ValueType>(markovModel, properties, onlyInitialStatesRelevant);
+                }
             } else {
                 verifySymbolicModelWithDdEngine<LibraryType, ValueType>(markovModel, properties, onlyInitialStatesRelevant);
             }
diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp
index 4670fda66..c1905fb69 100644
--- a/src/storm/transformer/SymbolicToSparseTransformer.cpp
+++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp
@@ -4,12 +4,29 @@
 #include "storm/storage/dd/Add.h"
 #include "storm/storage/dd/Bdd.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
-
 #include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/utility/macros.h"
+#include "storm/exceptions/NotImplementedException.h"
 
 namespace storm {
     namespace transformer {
 
+        template<storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel) {
+            switch (symbolicModel->getType()) {
+                case storm::models::ModelType::Dtmc:
+                    return SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>().translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<Type, ValueType>>());
+                case storm::models::ModelType::Mdp:
+                    return SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Mdp<Type, ValueType>>());
+                case storm::models::ModelType::Ctmc:
+                    return SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<Type, ValueType>>());
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Transformation of symbolic " << symbolicModel->getType() << " to sparse model is not implemented.");
+            }
+            return nullptr;
+        }
+        
+
         template<storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc) {
             this->odd = symbolicDtmc.getReachableStates().createOdd();
@@ -106,19 +123,25 @@ namespace storm {
             return std::make_shared<storm::models::sparse::Ctmc<ValueType>>(transitionMatrix, labelling, rewardModels);
         }
 
+        template std::shared_ptr<storm::models::sparse::Model<double>> transformSymbolicToSparseModel<storm::dd::DdType::CUDD, double>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> const& symbolicModel);
+        template std::shared_ptr<storm::models::sparse::Model<double>> transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, double>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>> const& symbolicModel);
+        template std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, storm::RationalNumber>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalNumber>> const& symbolicModel);
+        template std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, storm::RationalFunction>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>> const& symbolicModel);
+        
         template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::CUDD, double>;
         template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, double>;
-        
         template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
         template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalFunction>;
         
         template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::CUDD, double>;
         template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, double>;
         template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+        template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 
         template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::CUDD, double>;
         template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, double>;
         template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 
     }
 }
diff --git a/src/storm/transformer/SymbolicToSparseTransformer.h b/src/storm/transformer/SymbolicToSparseTransformer.h
index 5f4bed6c4..b55eb7ea9 100644
--- a/src/storm/transformer/SymbolicToSparseTransformer.h
+++ b/src/storm/transformer/SymbolicToSparseTransformer.h
@@ -12,6 +12,9 @@
 namespace storm {
     namespace transformer {
 
+        template<storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel);
+        
         template<storm::dd::DdType Type, typename ValueType>
         class SymbolicDtmcToSparseDtmcTransformer {
         public:
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index 61195bec0..fcc9e54c3 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -332,6 +332,7 @@ namespace storm {
             STORM_PRINT_AND_LOG("Transforming continuous model to discrete model...");
             storm::transformer::transformContinuousToDiscreteModelInPlace(markovModel, consideredFormula);
             STORM_PRINT_AND_LOG(" done!" << std::endl);
+            markovModel->printModelInformationToStream(std::cout);
         }
         
         auto modelParameters = storm::models::sparse::getProbabilityParameters(*markovModel);