diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 32362426f..916611aff 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -69,8 +69,6 @@ namespace storm { 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"); STORM_LOG_THROW(parsedStructure.at("automata").is_array(), storm::exceptions::InvalidJaniException, "Automata must be an array"); for(auto const& automataEntry : parsedStructure.at("automata")) { @@ -105,7 +103,7 @@ namespace storm { } } // TODO support other types. if(variableStructure.at("type").is_object()) { - + // STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::excepti } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); @@ -120,7 +118,7 @@ namespace storm { return expressionManager->boolean(false); } } else if(expressionStructure.is_number()) { - std::string stringrepr = expressionStructure.get(); + std::string stringrepr = expressionStructure.dump(); try { // It has to be an integer whenever it represents an integer. int64_t intval = boost::lexical_cast(stringrepr); @@ -139,7 +137,8 @@ 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(actionEntry.count("name") == 1, storm::exceptions::InvalidJaniException, "Actions must have exactly one name."); + std::string actionName = getString(actionEntry.at("name"), "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); diff --git a/test/functional/parser/JaniParserTest.cpp b/test/functional/parser/JaniParserTest.cpp index 0f900c64c..20dbf08a7 100644 --- a/test/functional/parser/JaniParserTest.cpp +++ b/test/functional/parser/JaniParserTest.cpp @@ -1,4 +1,20 @@ -// -// Created by Sebastian Junges on 21/05/16. -// +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/JaniParser.h" +#include "src/storage/jani/Model.h" + +TEST(JaniParser, DieTest) { + std::string testFileInput = STORM_CPP_TESTS_BASE_PATH"/../examples/jani-examples/dice.jani"; + storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput); +} + +TEST(JaniParser, BrpTest) { + std::string testFileInput = STORM_CPP_TESTS_BASE_PATH"/../examples/jani-examples/brp.jani"; + storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput); +} + +TEST(JaniParser, ConsensusTest) { + std::string testFileInput = STORM_CPP_TESTS_BASE_PATH"/../examples/jani-examples/consensus-6.jani"; + storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput); +} \ No newline at end of file