From 4df9984b87c950f707ab654d898eea98f1e292ef Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 20 May 2016 22:15:10 +0200 Subject: [PATCH] added bare minimum for parser calls Former-commit-id: b876e6dfa3db7fa8171ad0726c9a4ca6ead973ea --- src/parser/JaniParser.cpp | 29 ++++++++++++++++++++++++++--- src/parser/JaniParser.h | 39 +++++++++++++++++++++++++++++++++++---- src/storage/jani/Model.h | 25 +++++++++++++++++++++---- src/utility/storm.cpp | 11 ++++++++++- src/utility/storm.h | 5 ++++- 5 files changed, 96 insertions(+), 13 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index ae82bc147..afc79a909 100644 --- a/src/parser/JaniParser.cpp +++ b/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 +#include + +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(); + + } + } +} \ No newline at end of file diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index af73ed7f6..274cb2885 100644 --- a/src/parser/JaniParser.h +++ b/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 +#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 diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 74dda5762..062ab9125 100644 --- a/src/storage/jani/Model.h +++ b/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 automata; + std::map 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; } } diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index 3f1c713b5..a1fcaf5b2 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -1,3 +1,4 @@ +#include #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 diff --git a/src/utility/storm.h b/src/utility/storm.h index ce213cf08..9f909c815 100644 --- a/src/utility/storm.h +++ b/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> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::none, boost::optional const& transitionRewardsFile = boost::none, boost::optional 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> parseFormulasForExplicit(std::string const& inputString); std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);