diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm/parser/DeterministicSparseTransitionParser.cpp index 0a5d47616..ad56745bd 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm/parser/DeterministicSparseTransitionParser.cpp @@ -46,7 +46,7 @@ namespace storm { char const* buf = file.getData(); // Perform first pass, i.e. count entries that are not zero. - DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.getData()); + DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.getData(), !isRewardFile); STORM_LOG_TRACE("First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " non-zeros."); @@ -163,7 +163,7 @@ namespace storm { } template - typename DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char const* buf) { + typename DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char const* buf, bool reserveDiagonalElements) { DeterministicSparseTransitionParser::FirstPassResult result; @@ -180,7 +180,7 @@ namespace storm { // Read first row and reserve space for self-loops if necessary. char const* tmp; row = checked_strtol(buf, &tmp); - if (row > 0) { + if (row > 0 && reserveDiagonalElements) { for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) { ++result.numberOfNonzeroEntries; } @@ -193,7 +193,7 @@ namespace storm { // The actual read value is not needed here. checked_strtod(buf, &buf); - if (lastRow != row) { + if (lastRow != row && reserveDiagonalElements) { // Compensate for missing rows. for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { ++result.numberOfNonzeroEntries; @@ -218,10 +218,12 @@ namespace storm { buf = trimWhitespaces(buf); } - for (uint_fast64_t skippedRow = (uint_fast64_t) (lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) { - ++result.numberOfNonzeroEntries; + if (reserveDiagonalElements) { + for (uint_fast64_t skippedRow = (uint_fast64_t) (lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) { + ++result.numberOfNonzeroEntries; + } } - + return result; } diff --git a/src/storm/parser/DeterministicSparseTransitionParser.h b/src/storm/parser/DeterministicSparseTransitionParser.h index 0d830d2f9..d8ee3c447 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.h +++ b/src/storm/parser/DeterministicSparseTransitionParser.h @@ -65,9 +65,11 @@ namespace storm { * transitions and the maximum node id. * * @param buffer The buffer that contains the input. + * @param reserveDiagonalElements A flag indicating whether the diagonal elements should be counted as if they + * were present to enable fixes later. * @return A structure representing the result of the first pass. */ - static FirstPassResult firstPass(char const* buffer); + static FirstPassResult firstPass(char const* buffer, bool reserveDiagonalElements); /* * The main parsing routine.