From 11b04c794032e5d2de3810fe18ca070f19e44c0d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 27 Oct 2015 17:43:54 +0100
Subject: [PATCH] more work towards making the new bisim class available from
 the cl

Former-commit-id: b177287e001f3864eb100ea990a5893f8b5d12a8
---
 src/cli/entrypoints.h    | 33 +++++++++++++++++++++++++++++----
 src/models/ModelBase.cpp |  4 ++++
 src/models/ModelBase.h   |  8 ++++++++
 src/utility/storm.h      |  5 +----
 4 files changed, 42 insertions(+), 8 deletions(-)

diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index f541ef4d2..bcbf8cdfa 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -3,7 +3,6 @@
 
 #include "src/utility/storm.h"
 
-
 namespace storm {
     namespace cli {
 
@@ -84,14 +83,40 @@ namespace storm {
                 }
             }
         }
-
+        
+#define BRANCH_ON_MODELTYPE(result, model, value_type, dd_type, function, ...) \
+    if (model->isSymbolicModel()) { \
+        if (model->isOfType(storm::models::ModelType::Dtmc)) { \
+            result = function<storm::models::symbolic::Dtmc<dd_type>>(model->as<storm::models::symbolic::Dtmc<dd_type>>(), __VA_ARGS__); \
+        } else if (model->isOfType(storm::models::ModelType::Ctmc)) { \
+            result = function<storm::models::symbolic::Ctmc<dd_type>>(model->as<storm::models::symbolic::Ctmc<dd_type>>(), __VA_ARGS__); \
+        } else if (model->isOfType(storm::models::ModelType::Mdp)) { \
+            result = function<storm::models::symbolic::Mdp<dd_type>>(model->as<storm::models::symbolic::Mdp<dd_type>>(), __VA_ARGS__); \
+        } else { \
+            STORM_LOG_ASSERT(false, "Unknown model type."); \
+        } \
+    } else { \
+        STORM_LOG_ASSERT(model->isSparseModel(), "Unknown model type."); \
+        if (model->isOfType(storm::models::ModelType::Dtmc)) { \
+            result = function<storm::models::sparse::Dtmc<value_type>>(model->as<storm::models::sparse::Dtmc<value_type>>(), __VA_ARGS__); \
+        } else if (model->isOfType(storm::models::ModelType::Ctmc)) { \
+            result = function<storm::models::sparse::Ctmc<value_type>>(model->as<storm::models::sparse::Ctmc<value_type>>(), __VA_ARGS__); \
+        } else if (model->isOfType(storm::models::ModelType::Mdp)) { \
+            result = function<storm::models::sparse::Mdp<value_type>>(model->as<storm::models::sparse::Mdp<value_type>>(), __VA_ARGS__); \
+        } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { \
+            result = function<storm::models::sparse::MarkovAutomaton<value_type>>(model->as<storm::models::sparse::MarkovAutomaton<value_type>>(), __VA_ARGS__); \
+        } else { \
+            STORM_LOG_ASSERT(false, "Unknown model type."); \
+        } \
+    }
+    
         template<typename ValueType>
         void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
             std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(program, formulas);
             STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
 
             // Preprocess the model if needed.
-            model = preprocessModel<ValueType>(model, formulas);
+            BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas);
 
             // Print some information about the model.
             model->printModelInformationToStream(std::cout);
@@ -127,7 +152,7 @@ namespace storm {
             std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional<std::string>());
             
             // Preprocess the model if needed.
-            model = preprocessModel<ValueType>(model, formulas);
+            BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas);
 
             // Print some information about the model.
             model->printModelInformationToStream(std::cout);
diff --git a/src/models/ModelBase.cpp b/src/models/ModelBase.cpp
index 1eff87d18..b79d7a81f 100644
--- a/src/models/ModelBase.cpp
+++ b/src/models/ModelBase.cpp
@@ -13,5 +13,9 @@ namespace storm {
         bool ModelBase::isSymbolicModel() const {
             return false;
         }
+        
+        bool ModelBase::isOfType(storm::models::ModelType const& modelType) const {
+            return this->getType() == modelType;
+        }
     }
 }
\ No newline at end of file
diff --git a/src/models/ModelBase.h b/src/models/ModelBase.h
index 4bbe31b64..d118e1516 100644
--- a/src/models/ModelBase.h
+++ b/src/models/ModelBase.h
@@ -89,6 +89,14 @@ namespace storm {
              */
             virtual bool isSymbolicModel() const;
             
+            /*!
+             * Checks whether the model is of the given type.
+             *
+             * @param modelType The model type to check for.
+             * @return True iff the model is of the given type.
+             */
+            bool isOfType(storm::models::ModelType const& modelType) const;
+            
         private:
             // The type of the model.
             ModelType modelType;
diff --git a/src/utility/storm.h b/src/utility/storm.h
index c7fe8581d..38e78f364 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -30,6 +30,7 @@
 #include "src/models/ModelBase.h"
 #include "src/models/sparse/Model.h"
 #include "src/models/sparse/StandardRewardModel.h"
+#include "src/models/sparse/MarkovAutomaton.h"
 #include "src/models/symbolic/Model.h"
 #include "src/models/symbolic/StandardRewardModel.h"
 
@@ -80,8 +81,6 @@ namespace storm {
     std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString);
     std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
             
- 
- 
     template<typename ValueType>
     std::shared_ptr<storm::models::ModelBase> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
         std::shared_ptr<storm::models::ModelBase> result(nullptr);
@@ -111,7 +110,6 @@ namespace storm {
             result = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
         }
 
-        // Then, build the model from the symbolic description.
         return result;
     }
             
@@ -263,7 +261,6 @@ namespace storm {
         return result;
     }
             
-
 #endif
 
     template<storm::dd::DdType DdType>