From 584a79f974f306e992351b4c8c00cdef840f5216 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Feb 2014 17:47:03 +0100 Subject: [PATCH] Added proper creation of row grouping to nondeterministic model parser and the explicit model adapter. Former-commit-id: 723ddb2e1dc3936bbe37aee3180ae3bbf4d16ea6 --- src/adapters/ExplicitModelAdapter.h | 1 + ...NondeterministicSparseTransitionParser.cpp | 32 ++++++++++++++----- src/storage/SparseMatrix.cpp | 9 +++--- 3 files changed, 30 insertions(+), 12 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index aebbd1fcf..5a10795b6 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -543,6 +543,7 @@ namespace storm { // If the model is nondeterministic, we add all choices individually. nondeterministicChoiceIndices.push_back(currentRow); transitionMatrixBuilder.newRowGroup(currentRow); + transitionRewardMatrixBuilder.newRowGroup(currentRow); // First, process all unlabeled choices. for (auto const& choice : allUnlabeledChoices) { diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 02a1e94f1..cc7d99bfa 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -264,22 +264,22 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP * Those two values, as well as the number of nonzero elements, was been calculated in the first run. */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << choices << " x " << (maxnode+1) << " with " << nonzero << " entries."); - storm::storage::SparseMatrixBuilder matrixBuilder(choices, maxnode + 1, nonzero); - + storm::storage::SparseMatrixBuilder matrixBuilder(choices, maxnode + 1, nonzero, true); + /* * Create row mapping. */ std::vector rowMapping(maxnode + 2, 0); - + /* * Parse file content. */ int_fast64_t source, target, lastsource = -1, choice, lastchoice = -1; - uint_fast64_t curRow = -1; + int_fast64_t curRow = -1; double val; bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool hadDeadlocks = false; - + /* * Read all transitions from file. */ @@ -300,12 +300,14 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP // If we skipped some states, we need to reserve empty rows for all their nondeterministic // choices. for (int_fast64_t i = lastsource + 1; i < source; ++i) { + matrixBuilder.newRowGroup(curRow + 1); curRow += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]); } // If we advanced to the next state, but skipped some choices, we have to reserve rows // for them if (source != lastsource) { + matrixBuilder.newRowGroup(curRow + 1); curRow += choice + 1; } else if (choice != lastchoice) { curRow += choice - lastchoice; @@ -325,6 +327,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP hadDeadlocks = true; if (fixDeadlocks) { rowMapping.at(node) = curRow; + matrixBuilder.newRowGroup(curRow); matrixBuilder.addNextValue(curRow, node, 1); ++curRow; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); @@ -337,6 +340,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP * Add this source to rowMapping, if this is the first choice we encounter for this state. */ rowMapping.at(source) = curRow; + matrixBuilder.newRowGroup(curRow); } } @@ -373,9 +377,21 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP buf = trimWhitespaces(buf); } - for (int_fast64_t node = lastsource + 1; node <= maxnode + 1; node++) { - rowMapping.at(node) = curRow + 1; - } + if (isRewardFile) { + for (int_fast64_t node = lastsource + 1; node <= maxnode + 1; ++node) { + rowMapping.at(node) = curRow + 1; + if (node <= maxnode) { + matrixBuilder.newRowGroup((*rewardMatrixInformation->nondeterministicChoiceIndices)[node]); + } + } + } else { + for (int_fast64_t node = lastsource + 1; node <= maxnode + 1; ++node) { + rowMapping.at(node) = curRow + 1; + if (node <= maxnode) { + matrixBuilder.newRowGroup(curRow + 1); + } + } + } if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index cb62d529c..f9178b275 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -99,7 +99,9 @@ namespace storm { template void SparseMatrixBuilder::newRowGroup(uint_fast64_t startingRow) { if (!hasCustomRowGrouping) { - throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::addRowGroup: matrix was not created to have a custom row grouping."; + throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: matrix was not created to have a custom row grouping."; + } else if (rowGroupIndices.size() > 0 && startingRow < rowGroupIndices.back()) { + throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: illegal row group with negative size."; } if (rowGroupCountSet) { rowGroupIndices[currentRowGroup] = startingRow; @@ -837,9 +839,8 @@ namespace storm { // Check for matching sizes. if (this->getRowCount() != matrix.getRowCount()) return false; if (this->getColumnCount() != matrix.getColumnCount()) return false; - if (this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false; - + // Check the subset property for all rows individually. for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = matrix.begin(row), ite2 = matrix.end(row); it1 != ite1; ++it1) { @@ -866,7 +867,7 @@ namespace storm { // Iterate over all row groups. for (uint_fast64_t group = 0; group < matrix.getRowGroupCount(); ++group) { - out << "\t---- group " << group << " ----" << std::endl; + out << "\t---- group " << group << " ---- out of " << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl; for (uint_fast64_t i = matrix.getRowGroupIndices()[group]; i < matrix.getRowGroupIndices()[group + 1]; ++i) { uint_fast64_t nextIndex = matrix.rowIndications[i];