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 +#include #include 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 composition = parseComposition(parsedStructure.at("system")); + + + } + + storm::jani::Automaton JaniParser::parseAutomaton(json const &automatonStructure) { + + } + + std::shared_ptr 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 +#include #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 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; }