From 0afb73bba10167ba1864345093190e2995edea87 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 29 Mar 2014 14:42:29 +0100 Subject: [PATCH] refactoring of DetSparseTrans Parser to support parameters in future Former-commit-id: cf451cdf6183ae5d1f76fe34081cafc0341c019c --- .../DeterministicSparseTransitionParser.cpp | 172 ++++++++++-------- .../DeterministicSparseTransitionParser.h | 25 ++- src/parser/ReadValues.h | 24 +++ src/storage/SparseMatrix.cpp | 2 +- 4 files changed, 143 insertions(+), 80 deletions(-) create mode 100644 src/parser/ReadValues.h diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 67e31484f..47546c036 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -21,6 +21,8 @@ #include "src/exceptions/WrongFormatException.h" #include "src/settings/Settings.h" +#include "ReadValues.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -32,9 +34,9 @@ namespace storm { storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename) { - storm::storage::SparseMatrix emptyMatrix; - + storm::storage::SparseMatrix emptyMatrix; return DeterministicSparseTransitionParser::parse(filename, false, emptyMatrix); + } storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix const & transitionMatrix) { @@ -42,7 +44,8 @@ namespace storm { return DeterministicSparseTransitionParser::parse(filename, true, transitionMatrix); } - storm::storage::SparseMatrix DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const & transitionMatrix) { + template + storm::storage::SparseMatrix DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const & transitionMatrix) { // Enforce locale where decimal point is '.'. setlocale(LC_NUMERIC, "C"); @@ -67,15 +70,7 @@ namespace storm { throw storm::exceptions::WrongFormatException(); } - // Perform second pass. - - // Skip the format hint if it is there. - buf = trimWhitespaces(buf); - if(buf[0] < '0' || buf[0] > '9') { - buf = forwardToLineEnd(buf); - buf = trimWhitespaces(buf); - } - + if(isRewardFile) { // The reward matrix should match the size of the transition matrix. if (firstPass.highestStateIndex + 1 > transitionMatrix.getRowCount() || firstPass.highestStateIndex + 1 > transitionMatrix.getColumnCount()) { @@ -86,13 +81,18 @@ namespace storm { firstPass.highestStateIndex = transitionMatrix.getRowCount() - 1; } } + // Perform second pass. + + // Skip the format hint if it is there. + buf = skipFormatHint(buf); + // Creating matrix builder here. // The actual matrix will be build once all contents are inserted. storm::storage::SparseMatrixBuilder resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries); - uint_fast64_t row, col, lastRow = 0; - double val; + uint_fast64_t lastRow = 0; + DeterministicTransitionEntry trans; bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool hadDeadlocks = false; bool rowHadDiagonalEntry = false; @@ -105,84 +105,75 @@ namespace storm { // Different parsing routines for transition systems and transition rewards. if(isRewardFile) { while (buf[0] != '\0') { - // Read next transition. - row = checked_strtol(buf, &buf); - col = checked_strtol(buf, &buf); - val = checked_strtod(buf, &buf); - - resultMatrix.addNextValue(row, col, val); - buf = trimWhitespaces(buf); + readNextTransition(&buf, &trans); + addTransitionToMatrix(trans, &resultMatrix); } } else { while (buf[0] != '\0') { // Read next transition. - row = checked_strtol(buf, &buf); - col = checked_strtol(buf, &buf); - val = checked_strtod(buf, &buf); + readNextTransition(&buf, &trans); // 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::constantZero()); - LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)"); - } else { - LOG4CPLUS_WARN(logger, "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 (fixDeadlocks) { - resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); - rowHadDiagonalEntry = true; - LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); - } else { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions."); - // Before throwing the appropriate exception we will give notice of all deadlock states. - } - } - lastRow = row; - rowHadDiagonalEntry = false; - } - - if (col == row) { - rowHadDiagonalEntry = true; - } - - if (col > row && !rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(row, row, storm::utility::constantZero()); - LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); - } else { - LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself."); - } - rowHadDiagonalEntry = true; - } - - resultMatrix.addNextValue(row, col, val); - buf = trimWhitespaces(buf); + if (lastRow != trans.row) { + if (!rowHadDiagonalEntry) { + if (insertDiagonalEntriesIfMissing) { + resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); + LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)"); + } else { + LOG4CPLUS_WARN(logger, "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 < trans.row; ++skippedRow) { + hadDeadlocks = true; + if (fixDeadlocks) { + resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); + rowHadDiagonalEntry = true; + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); + } else { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions."); + // Before throwing the appropriate exception we will give notice of all deadlock states. + } + } + lastRow = trans.row; + rowHadDiagonalEntry = false; + } + + if (trans.col == trans.row) { + rowHadDiagonalEntry = true; + } + + if (trans.col > trans.row && !rowHadDiagonalEntry) { + if (insertDiagonalEntriesIfMissing) { + resultMatrix.addNextValue(trans.row, trans.row, storm::utility::constantZero()); + LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << trans.row << " has no transition to itself. Inserted a 0-transition. (2)"); + } else { + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << trans.row << " has no transition to itself."); + } + rowHadDiagonalEntry = true; + } + addTransitionToMatrix(trans, &resultMatrix); } if (!rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); + resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); } else { LOG4CPLUS_WARN(logger, "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 (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; + // If we encountered deadlock and did not fix them, now is the time to throw the exception. + if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; } // Finally, build the actual matrix, test and return it. - storm::storage::SparseMatrix result = resultMatrix.build(); + storm::storage::SparseMatrix result = resultMatrix.build(); // Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards. if(isRewardFile && !result.isSubmatrixOf(transitionMatrix)) { @@ -198,11 +189,7 @@ namespace storm { DeterministicSparseTransitionParser::FirstPassResult result; // Skip the format hint if it is there. - buf = trimWhitespaces(buf); - if(buf[0] < '0' || buf[0] > '9') { - buf = forwardToLineEnd(buf); - buf = trimWhitespaces(buf); - } + buf = skipFormatHint(buf); // Check all transitions for non-zero diagonal entries and deadlock states. uint_fast64_t row, col, lastRow = 0, lastCol = -1; @@ -213,7 +200,8 @@ namespace storm { row = checked_strtol(buf, &buf); col = checked_strtol(buf, &buf); // The actual read value is not needed here. - checked_strtod(buf, &buf); + buf = forwardToLineEnd(buf); + buf = trimWhitespaces(buf); // Compensate for missing diagonal entries if desired. if (insertDiagonalEntriesIfMissing) { @@ -254,7 +242,7 @@ namespace storm { lastRow = row; lastCol = col; - buf = trimWhitespaces(buf); + } if(insertDiagonalEntriesIfMissing) { @@ -270,6 +258,36 @@ namespace storm { return result; } + + template + void DeterministicSparseTransitionParser::readNextTransition(char** buf, DeterministicTransitionEntry* trans) + { + trans->row = checked_strtol(*buf, buf); + trans->col = checked_strtol(*buf, buf); + trans->val = checked_strtod(*buf, buf); + + *buf = trimWhitespaces(*buf); + } + + + + template + void DeterministicSparseTransitionParser::addTransitionToMatrix(DeterministicTransitionEntry const& trans, storm::storage::SparseMatrixBuilder* mat) + { + mat->addNextValue(trans.row, trans.col, trans.val); + } + + char* DeterministicSparseTransitionParser::skipFormatHint(char* buf) + { + // Skip the format hint if it is there. + buf = trimWhitespaces(buf); + if(buf[0] < '0' || buf[0] > '9') { + buf = forwardToLineEnd(buf); + buf = trimWhitespaces(buf); + } + return buf; + } + } // namespace parser } // namespace storm diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index e31ef2291..cddf1420c 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -5,7 +5,8 @@ namespace storm { namespace parser { - + + /*! * This class can be used to parse a file containing either transitions or transition rewards of a deterministic model. * @@ -16,6 +17,13 @@ namespace storm { class DeterministicSparseTransitionParser { public: + template + struct DeterministicTransitionEntry + { + uint_fast64_t row = 0; + uint_fast64_t col = 0; + T val; + }; /*! * A structure representing the result of the first pass of this parser. It contains the number of non-zero entries in the model and the highest state index. */ @@ -80,9 +88,22 @@ namespace storm { * The dimensions (rows and columns) of the two matrices should match. * @return A SparseMatrix containing the parsed file contents. */ - static storm::storage::SparseMatrix parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const & transitionMatrix); + template + static storm::storage::SparseMatrix parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const & transitionMatrix); + // Helper methods. + /* + */ + template + static void readNextTransition(char** buf, DeterministicTransitionEntry* trans ); + + + template + static void addTransitionToMatrix(DeterministicTransitionEntry const& trans, storm::storage::SparseMatrixBuilder* mat); + + static char* skipFormatHint(char*); }; + } // namespace parser } // namespace storm diff --git a/src/parser/ReadValues.h b/src/parser/ReadValues.h new file mode 100644 index 000000000..dad3b42b2 --- /dev/null +++ b/src/parser/ReadValues.h @@ -0,0 +1,24 @@ +#ifndef _STORM_PARSER_READVALUES_H +#define _STORM_PARSER_READVALUES_H + +#include "src/utility/cstring.h" + +namespace storm +{ + namespace parser + { + + template + T readValue(char* buf); + + template<> + double readValue(char* buf) + { + return utility::cstring::checked_strtod(buf, &buf); + } + + } +} + +#endif + diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 21814b643..28fa2dc5b 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -85,7 +85,7 @@ namespace storm { // Finally, set the element and increase the current size. if (storagePreallocated) { - columnsAndValues[currentEntryCount] = std::make_pair(column, value); + columnsAndValues.at(currentEntryCount) = std::make_pair(column, value); } else { columnsAndValues.emplace_back(column, value); if (!columnCountSet) {