diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm/parser/DeterministicSparseTransitionParser.cpp index 94a66b066..0a5d47616 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm/parser/DeterministicSparseTransitionParser.cpp @@ -176,7 +176,6 @@ namespace storm { // Check all transitions for non-zero diagonal entries and deadlock states. uint_fast64_t row, col, lastRow = 0, lastCol = -1; - bool rowHadDiagonalEntry = false; // Read first row and reserve space for self-loops if necessary. char const* tmp; @@ -188,13 +187,19 @@ namespace storm { } while (buf[0] != '\0') { - // Read the transition. row = checked_strtol(buf, &buf); col = checked_strtol(buf, &buf); // The actual read value is not needed here. checked_strtod(buf, &buf); + if (lastRow != row) { + // Compensate for missing rows. + for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { + ++result.numberOfNonzeroEntries; + } + } + // Check if a higher state id was found. if (row > result.highestStateIndex) result.highestStateIndex = row; if (col > result.highestStateIndex) result.highestStateIndex = col; @@ -213,6 +218,10 @@ namespace storm { buf = trimWhitespaces(buf); } + for (uint_fast64_t skippedRow = (uint_fast64_t) (lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) { + ++result.numberOfNonzeroEntries; + } + return result; } diff --git a/src/test/parser/DeterministicSparseTransitionParserTest.cpp b/src/test/parser/DeterministicSparseTransitionParserTest.cpp index a2a954bd1..bd8e9e2f2 100644 --- a/src/test/parser/DeterministicSparseTransitionParserTest.cpp +++ b/src/test/parser/DeterministicSparseTransitionParserTest.cpp @@ -33,29 +33,20 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) { storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_general.tra"); ASSERT_EQ(8ul, transitionMatrix.getColumnCount()); - ASSERT_EQ(21ul, transitionMatrix.getEntryCount()); + ASSERT_EQ(17ul, transitionMatrix.getEntryCount()); // Test every entry of the matrix. storm::storage::SparseMatrix::const_iterator cIter = transitionMatrix.begin(0); - ASSERT_EQ(0ul, cIter->getColumn()); - ASSERT_EQ(0, cIter->getValue()); - cIter++; ASSERT_EQ(1ul, cIter->getColumn()); ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(1ul, cIter->getColumn()); - ASSERT_EQ(0, cIter->getValue()); - cIter++; ASSERT_EQ(2ul, cIter->getColumn()); ASSERT_EQ(0.5, cIter->getValue()); cIter++; ASSERT_EQ(3ul, cIter->getColumn()); ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(2ul, cIter->getColumn()); - ASSERT_EQ(0, cIter->getValue()); - cIter++; ASSERT_EQ(3ul, cIter->getColumn()); ASSERT_EQ(0.4, cIter->getValue()); cIter++; @@ -71,9 +62,6 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) { ASSERT_EQ(3ul, cIter->getColumn()); ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(4ul, cIter->getColumn()); - ASSERT_EQ(0, cIter->getValue()); - cIter++; ASSERT_EQ(3ul, cIter->getColumn()); ASSERT_EQ(0.1, cIter->getValue()); cIter++; @@ -197,7 +185,7 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_deadlock.tra"); ASSERT_EQ(9ul, transitionMatrix.getColumnCount()); - ASSERT_EQ(23ul, transitionMatrix.getEntryCount()); + ASSERT_EQ(18ul, transitionMatrix.getEntryCount()); storm::storage::SparseMatrix::const_iterator cIter = transitionMatrix.begin(7); ASSERT_EQ(7ul, cIter->getColumn()); @@ -208,9 +196,6 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { cIter++; ASSERT_EQ(7ul, cIter->getColumn()); ASSERT_EQ(0.775347, cIter->getValue()); - cIter++; - ASSERT_EQ(8ul, cIter->getColumn()); - ASSERT_EQ(0, cIter->getValue()); } TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) {