From 5e3a8a12326a6dd5cc336ab01c7bb86522e0691e Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 8 Mar 2013 16:21:15 +0100 Subject: [PATCH] Fixed wrong check for submatrix property of reward matrices. --- src/models/Dtmc.h | 9 ++++----- src/storage/SparseMatrix.h | 16 ++++++++++++++-- 2 files changed, 18 insertions(+), 7 deletions(-) diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 7f0a0bb89..eefcc2ab5 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -50,11 +50,10 @@ public: throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; } if (this->getTransitionRewardMatrix() != nullptr) { - // FIXME: This is temporarily commented out, because the checking routine does not work properly. - //if (!this->getTransitionRewardMatrix()->isSubmatrixOf(*(this->getTransitionMatrix()))) { - // LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); - // throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; - //} + if (!this->getTransitionRewardMatrix()->isSubmatrixOf(*(this->getTransitionMatrix()))) { + LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); + throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; + } } } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index bde75c354..f5c4c954f 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -865,16 +865,28 @@ public: * @param matrix Matrix to check against. * @return True iff this is a submatrix of matrix. */ - bool isSubmatrixOf(SparseMatrix const & matrix) const { - // FIXME: THIS DOES NOT IMPLEMENT WHAT IS PROMISED. + bool isSubmatrixOf(SparseMatrix const& matrix) const { if (this->getRowCount() != matrix.getRowCount()) return false; if (this->getColumnCount() != matrix.getColumnCount()) return false; + /* for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem, ++elem2) { if (columnIndications[elem] < matrix.columnIndications[elem2]) return false; } } + */ + + for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { + for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem) { + // Skip over all entries of the other matrix that are before the current entry in + // the current matrix. + while (elem2 < matrix.rowIndications[row + 1] && matrix.columnIndications[elem2] < columnIndications[elem]) { + ++elem2; + } + if (!(elem2 < matrix.rowIndications[row + 1]) || columnIndications[elem] != matrix.columnIndications[elem2]) return false; + } + } return true; }