Browse Source

more test-files included, two small fixes in parser

Former-commit-id: 0e9000c988
tempestpy_adaptions
sjunges 9 years ago
parent
commit
3b5c27acba
  1. 9
      src/parser/JaniParser.cpp
  2. 22
      test/functional/parser/JaniParserTest.cpp

9
src/parser/JaniParser.cpp

@ -69,8 +69,6 @@ namespace storm {
for(auto const& varStructure : parsedStructure.at("variables")) { for(auto const& varStructure : parsedStructure.at("variables")) {
parseVariable(varStructure, "global"); 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.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"); STORM_LOG_THROW(parsedStructure.at("automata").is_array(), storm::exceptions::InvalidJaniException, "Automata must be an array");
for(auto const& automataEntry : parsedStructure.at("automata")) { for(auto const& automataEntry : parsedStructure.at("automata")) {
@ -105,7 +103,7 @@ namespace storm {
} }
} // TODO support other types. } // TODO support other types.
if(variableStructure.at("type").is_object()) { if(variableStructure.at("type").is_object()) {
// STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::excepti
} }
else { else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); 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); return expressionManager->boolean(false);
} }
} else if(expressionStructure.is_number()) { } else if(expressionStructure.is_number()) {
std::string stringrepr = expressionStructure.get<std::string>();
std::string stringrepr = expressionStructure.dump();
try { try {
// It has to be an integer whenever it represents an integer. // It has to be an integer whenever it represents an integer.
int64_t intval = boost::lexical_cast<int64_t>(stringrepr); int64_t intval = boost::lexical_cast<int64_t>(stringrepr);
@ -139,7 +137,8 @@ namespace storm {
void JaniParser::parseActions(json const& actionStructure, storm::jani::Model& parentModel) { void JaniParser::parseActions(json const& actionStructure, storm::jani::Model& parentModel) {
std::set<std::string> actionNames; std::set<std::string> actionNames;
for(auto const& actionEntry : actionStructure) { 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."); STORM_LOG_THROW(actionNames.count(actionName) == 0, storm::exceptions::InvalidJaniException, "Action with name " + actionName + " already exists.");
parentModel.addAction(storm::jani::Action(actionName)); parentModel.addAction(storm::jani::Action(actionName));
actionNames.emplace(actionName); actionNames.emplace(actionName);

22
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);
}
Loading…
Cancel
Save