diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 474e43a58..f34f47c43 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -2,6 +2,7 @@ #include "src/storage/jani/Model.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/InvalidJaniException.h" +#include "src/storage/jani/ModelType.h" #include #include @@ -45,6 +46,19 @@ namespace storm { } storm::jani::Model JaniParser::parseModel() { + STORM_LOG_THROW(parsedStructure.count("jani-version") == 1, storm::exceptions::InvalidJaniException, "Jani-version must be given exactly once."); + + STORM_LOG_THROW(parsedStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "A type must be given exactly once"); + std::string modeltypestring = getString(parsedStructure.at("type"), "type of the model"); + 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("model", type); + + 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("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"); @@ -58,6 +72,16 @@ namespace storm { } + void JaniParser::parseActions(json const& actionStructure, storm::jani::Model& parentModel) { + std::set actionNames; + for(auto const& actionEntry : actionStructure) { + std::string actionName = getString(actionEntry, "name of action"); + STORM_LOG_THROW(actionNames.count(actionName) == 0, storm::exceptions::InvalidJaniException, "Action with name " + actionName + " already exists."); + parentModel.addAction(storm::jani::Action(actionName)); + actionNames.emplace(actionName); + } + } + storm::jani::Automaton JaniParser::parseAutomaton(json const &automatonStructure) { STORM_LOG_THROW(automatonStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Each automaton must have a name"); std::string name = getString(parsedStructure.at("name"), " the name field for automaton"); @@ -72,6 +96,8 @@ namespace storm { } + + return automaton; } diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index cb0432f55..c36f6e5d3 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -31,6 +31,7 @@ namespace storm { void readFile(std::string const& path); storm::jani::Model parseModel(); storm::jani::Automaton parseAutomaton(json const& automatonStructure); + void parseActions(json const& actionStructure, storm::jani::Model& parentModel); std::shared_ptr parseComposition(json const& compositionStructure);