From 160a2c32a2ca235829f12b0ee11d28b544ec4ccc Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Mon, 17 Aug 2020 14:51:19 +0200
Subject: [PATCH] added SMGs to existing ModelTypes

---
 src/storm/builder/ExplicitModelBuilder.cpp | 12 +++++++-----
 src/storm/models/ModelType.cpp             |  5 +++++
 src/storm/models/ModelType.h               |  4 ++--
 src/storm/utility/builder.cpp              |  7 +++++--
 4 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index 8fedf075b..2b120f8ac 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -80,22 +80,24 @@ namespace storm {
                     return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Pomdp, buildModelComponents());
                 case storm::generator::ModelType::MA:
                     return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::MarkovAutomaton, buildModelComponents());
+                case storm::generator::ModelType::SMG:
+                    return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Smg, buildModelComponents());
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model: cannot handle this model type.");
             }
-            
+
             return nullptr;
         }
-        
+
         template <typename ValueType, typename RewardModelType, typename StateType>
         StateType ExplicitModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex(CompressedState const& state) {
             StateType newIndex = static_cast<StateType>(stateStorage.getNumberOfStates());
-            
+
             // Check, if the state was already registered.
             std::pair<StateType, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
-            
+
             StateType actualIndex = actualIndexBucketPair.first;
-            
+
             if (actualIndex == newIndex) {
                 if (options.explorationOrder == ExplorationOrder::Dfs) {
                     statesToExplore.emplace_front(state, actualIndex);
diff --git a/src/storm/models/ModelType.cpp b/src/storm/models/ModelType.cpp
index d556448bb..1e89ec163 100644
--- a/src/storm/models/ModelType.cpp
+++ b/src/storm/models/ModelType.cpp
@@ -19,6 +19,8 @@ namespace storm {
                 return ModelType::S2pg;
             } else if (type == "POMDP") {
                 return ModelType::Pomdp;
+            } else if (type == "SMG") {
+                return ModelType::Smg;
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Type " << type << "not known.");
             }
@@ -44,6 +46,9 @@ namespace storm {
                 case ModelType::Pomdp:
                     os << "POMDP";
                     break;
+                case ModelType::Smg:
+                    os << "Smg";
+                    break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unknown model type.");
             }
diff --git a/src/storm/models/ModelType.h b/src/storm/models/ModelType.h
index b183a598d..d9d7b0dc8 100644
--- a/src/storm/models/ModelType.h
+++ b/src/storm/models/ModelType.h
@@ -7,11 +7,11 @@ namespace storm {
     namespace models {
         // All supported model types.
         enum class ModelType {
-            Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg, Pomdp
+            Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg, Pomdp, Smg
         };
 
         ModelType getModelType(std::string const& type);
-        
+
         std::ostream& operator<<(std::ostream& os, ModelType const& type);
     }
 }
diff --git a/src/storm/utility/builder.cpp b/src/storm/utility/builder.cpp
index 481ed8020..0caa0edb3 100644
--- a/src/storm/utility/builder.cpp
+++ b/src/storm/utility/builder.cpp
@@ -6,13 +6,14 @@
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/Pomdp.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/Smg.h"
 
 #include "storm/exceptions/InvalidModelException.h"
 
 namespace storm {
     namespace utility {
         namespace builder {
-            
+
             template<typename ValueType, typename RewardModelType>
             std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components) {
                 switch (modelType) {
@@ -28,10 +29,12 @@ namespace storm {
                         return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>>(std::move(components));
                     case storm::models::ModelType::S2pg:
                         return std::make_shared<storm::models::sparse::StochasticTwoPlayerGame<ValueType, RewardModelType>>(std::move(components));
+                    case storm::models::ModelType::Smg:
+                        return std::make_shared<storm::models::sparse::Smg<ValueType, RewardModelType>>(std::move(components));
                 }
                 STORM_LOG_THROW(false, storm::exceptions::InvalidModelException, "Unknown model type");
             }
-            
+
             template std::shared_ptr<storm::models::sparse::Model<double>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<double>&& components);
             template std::shared_ptr<storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<storm::Interval>>&& components);
             template std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<storm::RationalNumber>&& components);