From c595fee4dc139c5cb58f54afba5cc507c8198aa5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 19 May 2017 13:04:16 +0200 Subject: [PATCH] removed some unnecessary transition insertions in parser --- .../DeterministicSparseTransitionParser.cpp | 75 +------------------ .../DeterministicSparseTransitionParser.h | 3 +- 2 files changed, 3 insertions(+), 75 deletions(-) diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm/parser/DeterministicSparseTransitionParser.cpp index 9aacb7e4c..94a66b066 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm/parser/DeterministicSparseTransitionParser.cpp @@ -46,8 +46,7 @@ namespace storm { char const* buf = file.getData(); // Perform first pass, i.e. count entries that are not zero. - bool insertDiagonalEntriesIfMissing = !isRewardFile; - DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.getData(), insertDiagonalEntriesIfMissing); + DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.getData()); STORM_LOG_TRACE("First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " non-zeros."); @@ -85,7 +84,6 @@ namespace storm { double val; bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); bool hadDeadlocks = false; - bool rowHadDiagonalEntry = false; // Read all transitions from file. Note that we assume that the // transitions are listed in canonical order, otherwise this will not @@ -131,16 +129,6 @@ namespace storm { // Test if we moved to a new row. // Handle all incomplete or skipped rows. if (lastRow != row) { - if (!rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::zero()); - STORM_LOG_DEBUG("While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)"); - } else { - STORM_LOG_WARN("Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); - } - // No increment for lastRow. - rowHadDiagonalEntry = true; - } for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { hadDeadlocks = true; if (!dontFixDeadlocks) { @@ -152,36 +140,12 @@ namespace storm { } } lastRow = row; - rowHadDiagonalEntry = false; - } - - if (col == row) { - rowHadDiagonalEntry = true; - } - - if (col > row && !rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(row, row, storm::utility::zero()); - STORM_LOG_DEBUG("While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); - } else { - STORM_LOG_WARN("Warning while parsing " << filename << ": state " << row << " has no transition to itself."); - } - rowHadDiagonalEntry = true; } resultMatrix.addNextValue(row, col, val); buf = trimWhitespaces(buf); } - if (!rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::zero()); - STORM_LOG_DEBUG("While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); - } else { - STORM_LOG_WARN("Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); - } - } - // If we encountered deadlock and did not fix them, now is the time to throw the exception. if (dontFixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the states do not have outgoing transitions."; } @@ -199,7 +163,7 @@ namespace storm { } template - typename DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char const* buf, bool insertDiagonalEntriesIfMissing) { + typename DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char const* buf) { DeterministicSparseTransitionParser::FirstPassResult result; @@ -231,30 +195,6 @@ namespace storm { // The actual read value is not needed here. checked_strtod(buf, &buf); - // Compensate for missing diagonal entries if desired. - if (insertDiagonalEntriesIfMissing) { - if (lastRow != row) { - if (!rowHadDiagonalEntry) { - ++result.numberOfNonzeroEntries; - } - - // Compensate for missing rows. - for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { - ++result.numberOfNonzeroEntries; - } - rowHadDiagonalEntry = false; - } - - if (col == row) { - rowHadDiagonalEntry = true; - } - - if (col > row && !rowHadDiagonalEntry) { - rowHadDiagonalEntry = true; - ++result.numberOfNonzeroEntries; - } - } - // Check if a higher state id was found. if (row > result.highestStateIndex) result.highestStateIndex = row; if (col > result.highestStateIndex) result.highestStateIndex = col; @@ -273,17 +213,6 @@ namespace storm { buf = trimWhitespaces(buf); } - if (insertDiagonalEntriesIfMissing) { - if (!rowHadDiagonalEntry) { - ++result.numberOfNonzeroEntries; - } - - //Compensate for missing rows at the end of the file. - 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 0515e120a..0d830d2f9 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.h +++ b/src/storm/parser/DeterministicSparseTransitionParser.h @@ -65,10 +65,9 @@ namespace storm { * transitions and the maximum node id. * * @param buffer The buffer that contains the input. - * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file. * @return A structure representing the result of the first pass. */ - static FirstPassResult firstPass(char const* buffer, bool insertDiagonalEntriesIfMissing = true); + static FirstPassResult firstPass(char const* buffer); /* * The main parsing routine.