Browse Source

Fixed two minor bugs.

- First one concerning the MappedFileTest in which I neglected to consider that the number of characters used to signal a new line differs between Linux (\n -> 1) and Windows (\r\n -> 2) which caused the test to fail on all OS using two characters (hence not on Linux, where I ran the tests).
- Second bug concerned the case that a transition reward file contained more states than the corresponding transition file.
  In that case the parser tried to acces the entry of the rowGroupIndices vector behind the last actual entry, which caused an exception to be thrown.
  Now there is a check whether the highest state index found by the parser does exceed the highest state index of the model.


Former-commit-id: bc83267f3c
tempestpy_adaptions
masawei 11 years ago
parent
commit
2ed6be853b
  1. 7
      src/parser/NondeterministicSparseTransitionParser.cpp
  2. 16
      test/functional/parser/MappedFileTest.cpp

7
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) {

16
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) {

Loading…
Cancel
Save