From 568cda29ed4408ed95e45d988fefeab1835423de Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 20 May 2016 23:02:14 +0200
Subject: [PATCH] more jani modelling stuff

Former-commit-id: fb834b7127668fc56fa276de0b8d5e5aa10262b8
---
 src/storage/jani/Model.cpp     | 15 +++++++++++
 src/storage/jani/Model.h       | 49 +++++++++++++++-------------------
 src/storage/jani/ModelType.cpp | 28 +++++++++++++++++++
 src/storage/jani/ModelType.h   | 13 +++++++++
 4 files changed, 77 insertions(+), 28 deletions(-)
 create mode 100644 src/storage/jani/ModelType.cpp
 create mode 100644 src/storage/jani/ModelType.h

diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index e69de29bb..337dd7c39 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -0,0 +1,15 @@
+#include "src/storage/jani/Model.h"
+
+namespace storm {
+    namespace jani {
+        
+        Model::Model(ModelType const& modelType, uint64_t version) : modelType(modelType), version(version) {
+            // Intentionally left empty.
+        }
+        
+        bool Model::isValid(bool logDebug) const {
+            // TODO.
+        }
+        
+    }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index 74dda5762..ad57f1bd8 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -1,38 +1,31 @@
 #pragma once
 
-#include "Automaton.h"
+#include "src/storage/jani/ModelType.h"
+#include "src/storage/jani/Automaton.h"
 
 namespace storm {
     namespace jani {
 
+        class Model {
+        public:
+            /*!
+             * Creates an empty model with the given type.
+             */
+            Model(ModelType const& modelType, uint64_t version = 1);
+            
+            /*!
+             * Checks whether the model is valid wrt. to the rules of JANI. Note that this does not make any statement
+             * about whether we can handle the model.
+             */
+            bool isValid(bool logdbg = true) const;
+            
+        private:
+            // The type of the model.
+            ModelType modelType;
+            
+            // The JANI-version used to specify the model.
+            uint64_t version;
 
-        class enum JaniModelType {UNSPECIFED = 0,
-                                    DTMC = 1,
-                                    CTMC = 2,
-                                    MDP = 3};
-
-        class JaniModel {
-            size_t janiVersion = 0;
-            JaniModelType modelType;
-            std::map<std::string, JaniAutomaton> automata;
-
-
-            bool checkValid(bool logdbg = true) {
-                if (janiVersion == 0) {
-                    if(logdbg) STORM_LOG_DEBUG("Jani version is unspecified");
-                    return false;
-                }
-
-                if(modelType == JaniModelType::UNSPECIFED) {
-                    if(logdbg) STORM_LOG_DEBUG("Model type is unspecified");
-                    return false;
-                }
-
-                if(automata.empty()) {
-                    if(logdbg) STORM_LOG_DEBUG("No automata specified");
-                }
-
-            }
         };
     }
 }
diff --git a/src/storage/jani/ModelType.cpp b/src/storage/jani/ModelType.cpp
new file mode 100644
index 000000000..243d69515
--- /dev/null
+++ b/src/storage/jani/ModelType.cpp
@@ -0,0 +1,28 @@
+#include "src/storage/jani/ModelType.h"
+
+namespace storm {
+    namespace jani {
+        
+        std::ostream& operator<<(std::ostream& stream, ModelType const& type) {
+            switch (type) {
+                case ModelType::UNDEFINED:
+                    stream << "undefined";
+                    break;
+                case ModelType::DTMC:
+                    stream << "dtmc";
+                    break;
+                case ModelType::CTMC:
+                    stream << "ctmc";
+                    break;
+                case ModelType::MDP:
+                    stream << "mdp";
+                    break;
+                case ModelType::MA:
+                    stream << "ma";
+                    break;
+            }
+            return stream;
+        }
+        
+    }
+}
diff --git a/src/storage/jani/ModelType.h b/src/storage/jani/ModelType.h
new file mode 100644
index 000000000..47568355e
--- /dev/null
+++ b/src/storage/jani/ModelType.h
@@ -0,0 +1,13 @@
+#pragma once
+
+#include <ostream>
+
+namespace storm {
+    namespace jani {
+        
+        enum class ModelType {UNDEFINED = 0, DTMC = 1, CTMC = 2, MDP = 3, MA = 4};
+     
+        std::ostream& operator<<(std::ostream& stream, ModelType const& type);
+        
+    }
+}
\ No newline at end of file