merge branch 'jani_support' of https://sselab.de/lab9/private/git/storm into jani_support

Former-commit-id: f9617835f2

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,24 +1,20 @@
 #pragma once
 
-#include "Automaton.h"
 #include "src/utility/macros.h"
 
+#include "src/storage/jani/ModelType.h"
+#include "src/storage/jani/Automaton.h"
 
 namespace storm {
     namespace jani {
 
-
-         enum class JaniModelType {UNSPECIFED = 0,
-                                    DTMC = 1,
-                                    CTMC = 2,
-                                    MDP = 3};
-
         class Model {
-            size_t janiVersion = 0;
-            JaniModelType modelType;
-            std::map<std::string, Automaton> automata;
-
         public:
+            /*!
+             * Creates an empty model with the given type.
+             */
+            Model(ModelType const& modelType, uint64_t version = 1);
+            
             /*!
              *  Does some simple checks to determine whether the model is supported by Prism.
              *  Mainly checks abscence of features the parser supports.
@@ -26,32 +22,24 @@ namespace storm {
              *  Throws UnsupportedModelException if something is wrong
              */
             // TODO add engine as argument to check this for several engines.
-            void checkSupported() {
+            void checkSupported();
 
-            }
-
-            /*!
+             /*!
              *  Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
              */
-            bool checkValidity(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");
-                    return false;
-                }
-                // All checks passed.
-                return true;
+             bool checkValidity(bool logdbg = true);
+        private:
+            /// The list of automata
+            std::vector<Automaton> automata;
+            /// A mapping from names to automata indices
+            std::map<std::string, size_t> automatonIndex;
+            /// The type of the model.
+            ModelType modelType;
+            /// The JANI-version used to specify the model.
+            uint64_t version;
+            /// The model name
+            std::string name;
 
-            }
         };
     }
 }

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