diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 7d6fbb527..32557dbb2 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -238,6 +238,13 @@ namespace storm { } if (isRewardFile) { + + // Make sure that the highest state index of the reward file is not higher than the highest state index of the corresponding model. + if(result.highestStateIndex > modelInformation.getColumnCount() - 1) { + LOG4CPLUS_ERROR(logger, "State index " << result.highestStateIndex << " found. This exceeds the highest state index of the model, which is " << modelInformation.getColumnCount() - 1 << " ."); + throw storm::exceptions::OutOfRangeException() << "State index " << result.highestStateIndex << " found. This exceeds the highest state index of the model, which is " << modelInformation.getColumnCount() - 1 << " ."; + } + // If we have switched the source state, we possibly need to insert rows for skipped choices of the last // source state. if (source != lastSource) { diff --git a/test/functional/parser/MappedFileTest.cpp b/test/functional/parser/MappedFileTest.cpp index a86ecb7cc..8b4d7bfba 100644 --- a/test/functional/parser/MappedFileTest.cpp +++ b/test/functional/parser/MappedFileTest.cpp @@ -10,6 +10,7 @@ #include <string> #include "src/parser/MappedFile.h" +#include "src/utility/cstring.h" #include "src/exceptions/FileIoException.h" TEST(MappedFileTest, NonExistingFile) { @@ -21,13 +22,18 @@ TEST(MappedFileTest, BasicFunctionality) { // Open a file and test if the content is loaded as expected. storm::parser::MappedFile file(STORM_CPP_TESTS_BASE_PATH "/functional/parser/testStringFile.txt"); - std::string testString = "This is a test string.\n"; - ASSERT_EQ(testString.length(), file.getDataEnd() - file.getData()); - char const * testStringPtr = testString.c_str(); - for(char* dataPtr = file.getData(); dataPtr < file.getDataEnd(); dataPtr++) { + std::string testString = "This is a test string."; + char * dataPtr = file.getData(); + for(char const * testStringPtr = testString.c_str(); testStringPtr - testString.c_str() < 22; testStringPtr++) { ASSERT_EQ(*testStringPtr, *dataPtr); - testStringPtr++; + dataPtr++; } + // The next character should be an end of line character (actual character varies between operating systems). + ASSERT_EQ(dataPtr, storm::utility::cstring::forwardToLineEnd(dataPtr)); + + // The newline character should be the last contained in the string. + ASSERT_EQ(file.getDataEnd(), storm::utility::cstring::forwardToNextLine(dataPtr)); + } TEST(MappedFileTest, ExistsAndReadble) {