diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 319d6b0cb..433c527ed 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -62,11 +62,12 @@ namespace storm { storm::jani::ModelType type = storm::jani::getModelType(modeltypestring); STORM_LOG_THROW(type != storm::jani::ModelType::UNDEFINED, storm::exceptions::InvalidJaniException, "model type " + modeltypestring + " not recognized"); storm::jani::Model model(name, type, version); - - STORM_LOG_THROW(parsedStructure.count("actions") < 2, storm::exceptions::InvalidJaniException, "Action-declarations can be given at most once"); + STORM_LOG_THROW(parsedStructure.count("actions") < 2, storm::exceptions::InvalidJaniException, "Action-declarations can be given at most once."); parseActions(parsedStructure.at("actions"), model); - - + STORM_LOG_THROW(parsedStructure.count("variables") < 2, storm::exceptions::InvalidJaniException, "Variable-declarations can be given at most once for global variables."); + for(auto const& varStructure : parsedStructure.at("variables")) { + parseVariable(varStructure, "global"); + } STORM_LOG_THROW(parsedStructure.count("automata") == 1, storm::exceptions::InvalidJaniException, "Exactly one list of automata must be given"); @@ -81,6 +82,41 @@ namespace storm { } + std::shared_ptr JaniParser::parseVariable(json const &variableStructure, std::string const& scopeDescription) { + STORM_LOG_THROW(variableStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Variable (scope: " + scopeDescription + ") must have a name"); + std::string name = getString(variableStructure.at("name"), "variable-name in " + scopeDescription + "-scope"); + STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration."); + STORM_LOG_THROW(variableStructure.count("initial-value") == 1, storm::exceptions::InvalidJaniException, "Initial value for variable '" + name + "' + (scope: " + scopeDescription + ") must be given once."); + // Read initial value before; that makes creation later on a bit easier, and has as an additional benefit that we do not need to check whether the variable occurs also on the assignment. + storm::expressions::Expression initExpr = parseExpression(variableStructure.at("initial-value"), "Initial value of variable " + name + " (scope: " + scopeDescription + ")"); + + if(variableStructure.at("type").is_string()) { + if(variableStructure.at("type") == "real") { + // expressionManager->declareRationalVariable(name); + } else if(variableStructure.at("type") == "bool") { + return std::make_shared(name, expressionManager->declareBooleanVariable(name), initExpr); + } else if(variableStructure.at("type") == "int") { + return std::make_shared(name, expressionManager->declareIntegerVariable(name), initExpr); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); + } + } // TODO support other types. + if(variableStructure.at("type").is_object()) { + + } + else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); + } + } + + storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription) { + STORM_LOG_WARN(scopeDescription); + //TDOO FIX + return expressionManager->boolean(false); + } + + + void JaniParser::parseActions(json const& actionStructure, storm::jani::Model& parentModel) { std::set actionNames; for(auto const& actionEntry : actionStructure) { diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index c36f6e5d3..f1cc262d1 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -1,9 +1,8 @@ #ifndef STORM_JANIPARSER_H #define STORM_JANIPARSER_H -#include -#include #include "src/exceptions/FileIoException.h" +#include "src/storage/expressions/ExpressionManager.h" // JSON parser #include "json.hpp" @@ -14,6 +13,8 @@ namespace storm { namespace jani { class Model; class Automaton; + class Variable; + class Composition; } @@ -21,9 +22,10 @@ namespace storm { class JaniParser { json parsedStructure; + std::shared_ptr expressionManager; public: - JaniParser() {} + JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {} JaniParser(std::string& jsonstring); static storm::jani::Model parse(std::string const& path); @@ -31,7 +33,14 @@ namespace storm { void readFile(std::string const& path); storm::jani::Model parseModel(); storm::jani::Automaton parseAutomaton(json const& automatonStructure); + std::shared_ptr parseVariable(json const& variableStructure, std::string const& scopeDescription); + storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription); + private: + /** + * Helper for parsing the actions of a model. + */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); + std::shared_ptr parseComposition(json const& compositionStructure);