From cf20e340de7a8e7a3fc1dbf3041a6894e6597b75 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 19 Aug 2020 16:05:39 +0200
Subject: [PATCH] Added a new enum that describes the model representation
 (sparse, dd with sylvan, dd with cudd).

---
 src/storm/models/ModelRepresentation.cpp | 26 +++++++++++++++
 src/storm/models/ModelRepresentation.h   | 42 ++++++++++++++++++++++++
 2 files changed, 68 insertions(+)
 create mode 100644 src/storm/models/ModelRepresentation.cpp
 create mode 100644 src/storm/models/ModelRepresentation.h

diff --git a/src/storm/models/ModelRepresentation.cpp b/src/storm/models/ModelRepresentation.cpp
new file mode 100644
index 000000000..e6f39d2ee
--- /dev/null
+++ b/src/storm/models/ModelRepresentation.cpp
@@ -0,0 +1,26 @@
+#include "storm/models/ModelRepresentation.h"
+
+#include "storm/exceptions/InvalidTypeException.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+    namespace models {
+
+        std::ostream& operator<<(std::ostream& os, ModelRepresentation const& representation) {
+            switch (representation) {
+                case ModelRepresentation::Sparse:
+                    os << "sparse";
+                    break;
+                case ModelRepresentation::DdCudd:
+                    os << "DD (Cudd)";
+                    break;
+                case ModelRepresentation::DdSylvan:
+                    os << "DD (Sylvan)";
+                    break;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unknown model representation.");
+            }
+            return os;
+        }
+    }
+}
diff --git a/src/storm/models/ModelRepresentation.h b/src/storm/models/ModelRepresentation.h
new file mode 100644
index 000000000..d26f14edb
--- /dev/null
+++ b/src/storm/models/ModelRepresentation.h
@@ -0,0 +1,42 @@
+#pragma once
+
+#include <ostream>
+
+#include "storm/storage/dd/DdType.h"
+
+namespace storm {
+    namespace models {
+        enum class ModelRepresentation {
+            Sparse, DdCudd, DdSylvan
+        };
+        std::ostream& operator<<(std::ostream& os, ModelRepresentation const& representation);
+        
+        template<storm::dd::DdType ddType>
+        struct GetModelRepresentation;
+        template<>
+        struct GetModelRepresentation<storm::dd::DdType::CUDD> {
+            static const ModelRepresentation representation = ModelRepresentation::DdCudd;
+        };
+        template<>
+        struct GetModelRepresentation<storm::dd::DdType::Sylvan> {
+            static const ModelRepresentation representation = ModelRepresentation::DdSylvan;
+        };
+        
+        template<ModelRepresentation representation>
+        struct GetDdType;
+        template<>
+        struct GetDdType<ModelRepresentation::Sparse> {
+            static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
+        };
+        template<>
+        struct GetDdType<ModelRepresentation::DdCudd> {
+            static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
+        };
+        template<>
+        struct GetDdType<ModelRepresentation::DdSylvan> {
+            static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
+        };
+        
+    }
+}
+