From 9a9cd968d9caac0b6dd3bcdb9012fd8f68bb4d72 Mon Sep 17 00:00:00 2001 From: PBerger Date: Thu, 31 Jan 2013 00:00:47 +0100 Subject: [PATCH] Added a test to verify the RowSum Function in the Sparse Matrix. Added an option to the settings for auto-fixing missing no-selfloop states. Kind of a super-option above fix-nodeadlocks, perhaps some Cleanup later on. Modified tra Files to comply with formats... --- .../DeterministicSparseTransitionParser.cpp | 83 +++++++++++++++---- src/storage/SparseMatrix.h | 9 +- src/utility/Settings.cpp | 1 + test/storage/SparseMatrixTest.cpp | 9 ++ 4 files changed, 84 insertions(+), 18 deletions(-) diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 632ac78ed..c5668846d 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -66,9 +66,10 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0; /* - * Check all transitions for non-zero diagonal entrys. + * Check all transitions for existing diagonal entrys. */ - int_fast64_t row, lastrow = -1, col; + int_fast64_t row, col; + int_fast64_t lastDiagonal = -1; double val; maxnode = 0; while (buf[0] != '\0') { @@ -80,17 +81,29 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast /* * Check if one is larger than the current maximum id. */ - if (row > maxnode) maxnode = row; - if (col > maxnode) maxnode = col; + if (row > maxnode) { + maxnode = row; + } + if (col > maxnode) { + maxnode = col; + } /* - * Check if a node was skipped, i.e. if a node has no outgoing - * transitions. If so, increase non_zero, as the second pass will + * Check if a self-loop was skipped. If so, increase non_zero, as the second pass will * either throw an exception (in this case, it doesn't matter * anyway) or add a self-loop (in this case, we'll need the * additional transition). */ - if (lastrow < row - 1) non_zero += row - lastrow - 1; - lastrow = row; + if (lastDiagonal < (row - 1)) { + non_zero += row - 1 - lastDiagonal; + lastDiagonal = row - 1; + } + /* + * Check if this is a self-loop and remember that + */ + if (row == col) { + lastDiagonal = row; + } + /* * Read probability of this transition. * Check, if the value is a probability, i.e. if it is between 0 and 1. @@ -103,6 +116,10 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast buf = trimWhitespaces(buf); } + if (lastDiagonal < (row - 1)) { + non_zero += row - 1 - lastDiagonal; + } + return non_zero; } @@ -171,12 +188,15 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st this->matrix->initialize(non_zero); int_fast64_t row, lastrow = -1, col; + int_fast64_t lastDiagonal = -1; double val; bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks"); + bool fixSelfloops = storm::settings::instance()->isSet("fix-selfloops"); bool hadDeadlocks = false; + bool hadNoSelfLoops = false; /* - * Read all transitions from file. Note that we assume, that the + * Read all transitions from file. Note that we assume that the * transitions are listed in canonical order, otherwise this will not * work, i.e. the values in the matrix will be at wrong places. */ @@ -189,24 +209,53 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st val = checked_strtod(buf, &buf); /* - * Check if we skipped a node, i.e. if a node does not have any - * outgoing transitions. + * Check if a self-loop was skipped. */ - for (int_fast64_t node = lastrow + 1; node < row; node++) { - hadDeadlocks = true; - if (fixDeadlocks) { - this->matrix->addNextValue(node, node, 1); - LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); + if (lastDiagonal < (row - 1)) { + /* + * Check if we skipped a node entirely, i.e. a node does not have any + * outgoing transitions. + */ + if ((lastrow + 1) < row) { + for (int_fast64_t node = lastrow + 1; node < row; node++) { + hadDeadlocks = true; + if (fixDeadlocks || fixSelfloops) { + this->matrix->addNextValue(node, node, storm::utility::constGetOne()); + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); + } else { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); + } + } } else { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); + // there were other transitions but no self-loop + for (int_fast64_t node = lastDiagonal + 1; node < row; node++) { + hadNoSelfLoops = true; + if (fixSelfloops) { + this->matrix->addNextValue(node, node, storm::utility::constGetZero()); + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no self transition. A self-loop was inserted."); + } else { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no self transition."); + } + } } + lastDiagonal = row - 1; + } + + + /* + * Check if this is a self-loop and remember that + */ + if (row == col) { + lastDiagonal = row; } + lastrow = row; this->matrix->addNextValue(row, col, val); buf = trimWhitespaces(buf); } if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; + if (!fixSelfloops && hadNoSelfLoops) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had no self loops. You can use --fix-selfloops to insert self-loops on the fly."; /* * Finalize Matrix. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index b7fa94d62..90807f1bc 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -799,22 +799,29 @@ public: /*! * Inverts all elements on the diagonal, i.e. sets the diagonal values to 1 minus their previous * value. + * Requires the matrix to contain each diagonal element AND to be square! */ void invertDiagonal() { if (this->getRowCount() != this->getColumnCount()) { throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!"; } - T one(1); + T one = storm::utility::constGetOne(); + bool foundRow; for (uint_fast64_t row = 0; row < rowCount; ++row) { uint_fast64_t rowStart = rowIndications[row]; uint_fast64_t rowEnd = rowIndications[row + 1]; + foundRow = false; while (rowStart < rowEnd) { if (columnIndications[rowStart] == row) { valueStorage[rowStart] = one - valueStorage[rowStart]; + foundRow = true; break; } ++rowStart; } + if (!foundRow) { + throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to contain all diagonal entries!"; + } } } diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 26f733071..f983f22fc 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -139,6 +139,7 @@ void Settings::initDescriptions() { ("transrew", bpo::value()->default_value(""), "name of transition reward file") ("staterew", bpo::value()->default_value(""), "name of state reward file") ("fix-deadlocks", "insert self-loops for states without outgoing transitions") + ("fix-selfloops", "insert self-loops for states without such transitions") ; } diff --git a/test/storage/SparseMatrixTest.cpp b/test/storage/SparseMatrixTest.cpp index 2a29fb736..b3eb68971 100644 --- a/test/storage/SparseMatrixTest.cpp +++ b/test/storage/SparseMatrixTest.cpp @@ -94,6 +94,10 @@ TEST(SparseMatrixTest, Test) { 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 /* second to last row */ }; + int row_sums[25] = {}; + for (int i = 0; i < 50; ++i) { + row_sums[position_row[i]] += values[i]; + } ASSERT_NO_THROW(ssm->initialize(50)); ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); @@ -123,6 +127,11 @@ TEST(SparseMatrixTest, Test) { } ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); + // Test Row Sums + for (int row = 0; row < 25; ++row) { + ASSERT_EQ(row_sums[row], ssm->getRowSum(row)); + } + delete ssm; }