more jani modelling stuff

Former-commit-id: fb834b7127

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.
+        }
+        
+    }
+}

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);
             
-        class enum JaniModelType {UNSPECIFED = 0,
-                                    DTMC = 1,
-                                    CTMC = 2,
-                                    MDP = 3};
+            /*!
+             * 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;
             
-        class JaniModel {
-            size_t janiVersion = 0;
-            JaniModelType modelType;
-            std::map<std::string, JaniAutomaton> automata;
+        private:
+            // The type of the model.
+            ModelType modelType;
             
+            // The JANI-version used to specify the model.
+            uint64_t version;
 
-            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");
-                }
-
-            }
         };
     }
 }

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;
+        }
+        
+    }
+}

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);
+        
+    }
+}