Browse Source

JaniParser:

return model with type and actions

Former-commit-id: 1fb028f90d
tempestpy_adaptions
sjunges 9 years ago
parent
commit
926d7730e5
  1. 26
      src/parser/JaniParser.cpp
  2. 1
      src/parser/JaniParser.h

26
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 <iostream>
#include <sstream>
@ -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<std::string> 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;
}

1
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<storm::jani::Composition> parseComposition(json const& compositionStructure);

Loading…
Cancel
Save