Browse Source

rough skeleton for the parser, v1

Former-commit-id: 1e53e99fbe
tempestpy_adaptions
sjunges 9 years ago
parent
commit
121cfe4d93
  1. 15
      src/exceptions/InvalidJaniException.h
  2. 35
      src/parser/JaniParser.cpp
  3. 7
      src/parser/JaniParser.h
  4. 2
      src/storage/jani/Model.h
  5. 4
      src/utility/storm.cpp

15
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

35
src/parser/JaniParser.cpp

@ -1,12 +1,25 @@
#include "JaniParser.h" #include "JaniParser.h"
#include "src/storage/jani/Model.h" #include "src/storage/jani/Model.h"
#include "src/exceptions/FileIoException.h" #include "src/exceptions/FileIoException.h"
#include "src/exceptions/InvalidJaniException.h"
#include <iostream> #include <iostream>
#include <sstream>
#include <fstream> #include <fstream>
namespace storm { namespace storm {
namespace parser { 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) { void JaniParser::readFile(std::string const &path) {
std::ifstream file; std::ifstream file;
file.exceptions ( std::ifstream::failbit ); file.exceptions ( std::ifstream::failbit );
@ -23,5 +36,27 @@ namespace storm {
file.close(); 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) {
}
} }
} }

7
src/parser/JaniParser.h

@ -2,6 +2,7 @@
#define STORM_JANIPARSER_H #define STORM_JANIPARSER_H
#include <src/storage/jani/Model.h> #include <src/storage/jani/Model.h>
#include <src/storage/jani/Composition.h>
#include "src/exceptions/FileIoException.h" #include "src/exceptions/FileIoException.h"
// JSON parser // JSON parser
@ -21,12 +22,16 @@ namespace storm {
json parsedStructure; json parsedStructure;
public:
JaniParser() {}
JaniParser(std::string& jsonstring);
static storm::jani::Model parse(std::string const& path); static storm::jani::Model parse(std::string const& path);
protected: protected:
void readFile(std::string const& path); void readFile(std::string const& path);
storm::jani::Model parseModel();
storm::jani::Automaton parseAutomaton(json const& automatonStructure); storm::jani::Automaton parseAutomaton(json const& automatonStructure);
std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure);

2
src/storage/jani/Model.h

@ -48,6 +48,8 @@ namespace storm {
if(logdbg) STORM_LOG_DEBUG("No automata specified"); if(logdbg) STORM_LOG_DEBUG("No automata specified");
return false; return false;
} }
// All checks passed.
return true;
} }
}; };

4
src/utility/storm.cpp

@ -4,7 +4,7 @@
// Headers related to parsing. // Headers related to parsing.
#include "src/parser/PrismParser.h" #include "src/parser/PrismParser.h"
#include "src/parser/FormulaParser.h" #include "src/parser/FormulaParser.h"
#include "src/utility/macros.h"
namespace storm { namespace storm {
@ -18,7 +18,7 @@ namespace storm {
storm::jani::Model parseJaniModel(std::string const& path) { storm::jani::Model parseJaniModel(std::string const& path) {
storm::jani::Model model = storm::parser::JaniParser::parse(path); storm::jani::Model model = storm::parser::JaniParser::parse(path);
if(!model.checkValidity(true)) { 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; return model;
} }

Loading…
Cancel
Save