added bare minimum for parser calls

Former-commit-id: b876e6dfa3

src/parser/JaniParser.cpp

@@ -1,4 +1,27 @@
-//
-// Created by Sebastian Junges on 20/05/16.
-//
+#include "JaniParser.h"
+#include "src/storage/jani/Model.h"
+#include "src/exceptions/FileIoException.h"
 
+#include <iostream>
+#include <fstream>
+
+namespace storm {
+    namespace parser {
+        void JaniParser::readFile(std::string const &path) {
+            std::ifstream file;
+            file.exceptions ( std::ifstream::failbit );
+            try {
+                file.open(path);
+            }
+            catch (std::ifstream::failure e) {
+                STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << path << ".");
+                return;
+            }
+            file.exceptions( std::ifstream::goodbit );
+
+            parsedStructure << file;
+            file.close();
+
+        }
+    }
+}

src/parser/JaniParser.h

@@ -1,8 +1,39 @@
-//
-// Created by Sebastian Junges on 18/05/16.
-//
-
 #ifndef STORM_JANIPARSER_H
 #define STORM_JANIPARSER_H
 
+#include <src/storage/jani/Model.h>
+#include "src/exceptions/FileIoException.h"
+
+// JSON parser
+#include "json.hpp"
+
+using json = nlohmann::json;
+
+namespace storm {
+    namespace jani {
+        class Model;
+        class Automaton;
+    }
+
+
+    namespace parser {
+        class JaniParser {
+
+            json parsedStructure;
+
+            static storm::jani::Model parse(std::string const& path);
+
+        protected:
+            void readFile(std::string const& path);
+            storm::jani::Automaton parseAutomaton(json const& automatonStructure);
+
+
+
+
+        };
+    }
+}
+
+
+
 #endif //STORM_JANIPARSER_H

src/storage/jani/Model.h

@@ -1,23 +1,39 @@
 #pragma once
 
 #include "Automaton.h"
+#include "src/utility/macros.h"
+
 
 namespace storm {
     namespace jani {
 
 
-        class enum JaniModelType {UNSPECIFED = 0,
+         enum class JaniModelType {UNSPECIFED = 0,
                                     DTMC = 1,
                                     CTMC = 2,
                                     MDP = 3};
 
-        class JaniModel {
+        class Model {
             size_t janiVersion = 0;
             JaniModelType modelType;
-            std::map<std::string, JaniAutomaton> automata;
+            std::map<std::string, Automaton> automata;
+
+        public:
+            /*!
+             *  Does some simple checks to determine whether the model is supported by Prism.
+             *  Mainly checks abscence of features the parser supports.
+             *
+             *  Throws UnsupportedModelException if something is wrong
+             */
+            // TODO add engine as argument to check this for several engines.
+            void checkSupported() {
 
+            }
 
-            bool checkValid(bool logdbg = true) {
+            /*!
+             *  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;
@@ -30,6 +46,7 @@ namespace storm {
 
                 if(automata.empty()) {
                     if(logdbg) STORM_LOG_DEBUG("No automata specified");
+                    return false;
                 }
 
             }

src/utility/storm.cpp

@@ -1,3 +1,4 @@
+#include <src/parser/JaniParser.h>
 #include "storm.h"
 
 // Headers related to parsing.
@@ -13,7 +14,15 @@ namespace storm {
         program.checkValidity();
         return program;
     }
-     
+
+    storm::jani::Model parseJaniModel(std::string const& path) {
+        storm::jani::Model model = storm::parser::JaniParser::parse(path);
+        if(!model.checkValidity(true)) {
+            STORM_LOG_THROW(storm::exceptions::FileIoException, "Jani file parsing yields invalid model.");
+        }
+        return model;
+    }
+
     /**
      * Helper
      * @param FormulaParser

src/utility/storm.h

@@ -43,6 +43,8 @@
 
 #include "src/parser/AutoParser.h"
 
+#include "src/storage/jani/Model.h"
+
 // Headers of builders.
 #include "src/builder/ExplicitPrismModelBuilder.h"
 #include "src/builder/DdPrismModelBuilder.h"
@@ -90,7 +92,8 @@ namespace storm {
     std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::none, boost::optional<std::string> const& transitionRewardsFile = boost::none, boost::optional<std::string> const& choiceLabelingFile = boost::none) {
         return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
     }
-            
+
+    storm::jani::Model parseModel(std::string const& path);
     storm::prism::Program parseProgram(std::string const& path);
     std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString);
     std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);