From 121cfe4d93d8418a05c803dbc71afe3305bb62a5 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Fri, 20 May 2016 23:06:10 +0200
Subject: [PATCH] rough skeleton for the parser, v1

Former-commit-id: 1e53e99fbef69cf6b8a9d508878059d8fdb0cf9e
---
 src/exceptions/InvalidJaniException.h | 15 ++++++++++++
 src/parser/JaniParser.cpp             | 35 +++++++++++++++++++++++++++
 src/parser/JaniParser.h               |  7 +++++-
 src/storage/jani/Model.h              |  2 ++
 src/utility/storm.cpp                 |  4 +--
 5 files changed, 60 insertions(+), 3 deletions(-)
 create mode 100644 src/exceptions/InvalidJaniException.h

diff --git a/src/exceptions/InvalidJaniException.h b/src/exceptions/InvalidJaniException.h
new file mode 100644
index 000000000..b3b0e35c1
--- /dev/null
+++ b/src/exceptions/InvalidJaniException.h
@@ -0,0 +1,15 @@
+#ifndef STORM_INVALIDJANIEXCEPTION_H
+#define STORM_INVALIDJANIEXCEPTION_H
+
+#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
+
+namespace storm {
+    namespace exceptions {
+
+        STORM_NEW_EXCEPTION(InvalidJaniException)
+
+    } // namespace exceptions
+} // namespace storm
+
+#endif //STORM_INVALIDJANIEXCEPTION_H
diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index afc79a909..7f7ee03fc 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -1,12 +1,25 @@
 #include "JaniParser.h"
 #include "src/storage/jani/Model.h"
 #include "src/exceptions/FileIoException.h"
+#include "src/exceptions/InvalidJaniException.h"
 
 #include <iostream>
+#include <sstream>
 #include <fstream>
 
 namespace storm {
     namespace parser {
+
+        storm::jani::Model JaniParser::parse(std::string const& path) {
+            JaniParser parser;
+            parser.readFile(path);
+            return parser.parseModel();
+        }
+
+        JaniParser::JaniParser(std::string &jsonstring) {
+            parsedStructure = json::parse(jsonstring);
+        }
+
         void JaniParser::readFile(std::string const &path) {
             std::ifstream file;
             file.exceptions ( std::ifstream::failbit );
@@ -23,5 +36,27 @@ namespace storm {
             file.close();
 
         }
+
+        storm::jani::Model JaniParser::parseModel() {
+
+            STORM_LOG_THROW(parsedStructure.count("automata") == 1, storm::exceptions::InvalidJaniException, "Exactly one list of automata must be given");
+            STORM_LOG_THROW(parsedStructure.at("automata").is_array(), storm::exceptions::InvalidJaniException, "Automata must be an array");
+            for(auto const& automataEntry : parsedStructure.at("automata")) {
+                storm::jani::Automaton automaton = parseAutomaton(automataEntry);
+
+            }
+            STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given");
+            std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system"));
+
+
+        }
+
+        storm::jani::Automaton JaniParser::parseAutomaton(json const &automatonStructure) {
+
+        }
+
+        std::shared_ptr<storm::jani::Composition> JaniParser::parseComposition(json const &compositionStructure) {
+            
+        }
     }
 }
\ No newline at end of file
diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h
index 274cb2885..cb0432f55 100644
--- a/src/parser/JaniParser.h
+++ b/src/parser/JaniParser.h
@@ -2,6 +2,7 @@
 #define STORM_JANIPARSER_H
 
 #include <src/storage/jani/Model.h>
+#include <src/storage/jani/Composition.h>
 #include "src/exceptions/FileIoException.h"
 
 // JSON parser
@@ -21,12 +22,16 @@ namespace storm {
 
             json parsedStructure;
 
+        public:
+            JaniParser() {}
+            JaniParser(std::string& jsonstring);
             static storm::jani::Model parse(std::string const& path);
 
         protected:
             void readFile(std::string const& path);
+            storm::jani::Model parseModel();
             storm::jani::Automaton parseAutomaton(json const& automatonStructure);
-
+            std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure);
 
 
 
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index 062ab9125..f287ab066 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -48,6 +48,8 @@ namespace storm {
                     if(logdbg) STORM_LOG_DEBUG("No automata specified");
                     return false;
                 }
+                // All checks passed.
+                return true;
 
             }
         };
diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp
index a1fcaf5b2..5956e72c9 100644
--- a/src/utility/storm.cpp
+++ b/src/utility/storm.cpp
@@ -4,7 +4,7 @@
 // Headers related to parsing.
 #include "src/parser/PrismParser.h"
 #include "src/parser/FormulaParser.h"
-
+#include "src/utility/macros.h"
 
 
 namespace storm {
@@ -18,7 +18,7 @@ namespace storm {
     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.");
+            STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Jani file parsing yields invalid model.");
         }
         return model;
     }