From 3fd72a11d8fcf0ca81c5efba31e1a45158666166 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 12 Jun 2017 12:07:27 +0200 Subject: [PATCH 1/4] Improved SparseMatrix::restrictRows so it can handle empty row groups --- src/storm/storage/SparseMatrix.cpp | 41 +++++++++++++++++++++++++----- src/storm/storage/SparseMatrix.h | 8 ++++-- 2 files changed, 40 insertions(+), 9 deletions(-) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index ed775b2b6..b8f694939 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -911,14 +911,41 @@ namespace storm { } template - SparseMatrix SparseMatrix::restrictRows(storm::storage::BitVector const& rowsToKeep) const { - // For now, we use the expensive call to submatrix. + SparseMatrix SparseMatrix::restrictRows(storm::storage::BitVector const& rowsToKeep, bool allowEmptyRowGroups) const { STORM_LOG_ASSERT(rowsToKeep.size() == this->getRowCount(), "Dimensions mismatch."); - STORM_LOG_ASSERT(rowsToKeep.getNumberOfSetBits() >= this->getRowGroupCount(), "Invalid dimensions."); - SparseMatrix res(getSubmatrix(false, rowsToKeep, storm::storage::BitVector(getColumnCount(), true), false)); - STORM_LOG_ASSERT(res.getRowCount() == rowsToKeep.getNumberOfSetBits(), "Invalid dimensions"); - STORM_LOG_ASSERT(res.getColumnCount() == this->getColumnCount(), "Invalid dimensions"); - STORM_LOG_ASSERT(this->getRowGroupCount() == res.getRowGroupCount(), "Invalid dimensions"); + + // Count the number of entries of the resulting matrix + uint_fast64_t entryCount = 0; + for (auto const& row : rowsToKeep) { + entryCount += this->getRow(row).getNumberOfEntries(); + } + + // build the matrix. The row grouping will always be considered as nontrivial. + SparseMatrixBuilder builder(rowsToKeep.getNumberOfSetBits(), this->getColumnCount(), entryCount, true, true, this->getRowGroupCount()); + uint_fast64_t newRow = 0; + for (uint_fast64_t rowGroup = 0; rowGroup < this->getRowGroupCount(); ++rowGroup) { + builder.newRowGroup(newRow); + bool rowGroupEmpty = true; + if (this->hasTrivialRowGrouping()) { + if (rowsToKeep.get(rowGroup)) { + rowGroupEmpty = false; + for (auto const& entry : this->getRow(rowGroup)) { + builder.addNextValue(newRow, entry.getColumn(), entry.getValue()); + } + ++newRow; + } + } else { + for (uint_fast64_t row = rowsToKeep.getNextSetIndex(this->getRowGroupIndices()[rowGroup]); row < this->getRowGroupIndices()[rowGroup + 1]; row = rowsToKeep.getNextSetIndex(row + 1)) { + rowGroupEmpty = false; + for (auto const& entry: this->getRow(row)) { + builder.addNextValue(newRow, entry.getColumn(), entry.getValue()); + } + ++newRow; + } + } + STORM_LOG_THROW(allowEmptyRowGroups || !rowGroupEmpty, storm::exceptions::InvalidArgumentException, "Empty rows are not allowed, but row group " << rowGroup << " is empty."); + } + SparseMatrix res = builder.build(); return res; } diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 19a63efe5..bd8c1bad1 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -657,9 +657,13 @@ namespace storm { * Restrict rows in grouped rows matrix. Ensures that the number of groups stays the same. * * @param rowsToKeep A bit vector indicating which rows to keep. - * + * @param allowEmptyRowGroups if set to true, the result can potentially have empty row groups. + * Otherwise, it is asserted that there are no empty row groups. + * + * @note The resulting matrix will always have a non-trivial row grouping even if the current one is trivial. + * */ - SparseMatrix restrictRows(storm::storage::BitVector const& rowsToKeep) const; + SparseMatrix restrictRows(storm::storage::BitVector const& rowsToKeep, bool allowEmptyRowGroups = false) const; /** * Compares two rows. From dcd9319ba409a519de0e2744866ec29541886456 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 12 Jun 2017 12:08:54 +0200 Subject: [PATCH 2/4] fixed a convertNumber instantiation --- src/storm/utility/constants.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 7e0e5309c..35d79c13f 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -99,7 +99,7 @@ namespace storm { template<> storm::storage::sparse::state_type convertNumber(long long const& number){ - return static_cast(number); + return static_cast(number); } template From 15b61b6d0fb2aef360303f0ba6f93bef27f5ddd0 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 12 Jun 2017 12:09:34 +0200 Subject: [PATCH 3/4] Fixed missing return statement for continuousToDiscreteTimeModelTransformer --- .../ContinuousToDiscreteTimeModelTransformer.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp index b27dc9524..0a1c03e4b 100644 --- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp +++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp @@ -10,6 +10,7 @@ #include "storm/utility/vector.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { namespace transformer { @@ -32,16 +33,18 @@ namespace storm { SparseCtmcToSparseDtmcTransformer transformer; if (transformer.transformationPreservesProperty(*formula)) { STORM_LOG_INFO("Transforming Ctmc to embedded Dtmc..."); - markovModel = transformer.translate(*markovModel->template as>(), timeRewardModelName); + return transformer.translate(*markovModel->template as>(), timeRewardModelName); } } else if (markovModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { SparseMaToSparseMdpTransformer transformer; if (transformer.transformationPreservesProperty(*formula)) { STORM_LOG_INFO("Transforming Markov automaton to embedded Mdp..."); - markovModel = transformer.translate(*markovModel->template as>(), timeRewardModelName); + return transformer.translate(*markovModel->template as>(), timeRewardModelName); } + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Model type " << markovModel->getType() << " not expected."); } - return markovModel; + return nullptr; } template @@ -70,6 +73,8 @@ namespace storm { STORM_LOG_INFO("Transforming Markov automaton to embedded Mdp..."); markovModel = transformer.translate(std::move(*markovModel->template as>()), timeRewardModelName); } + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Model type " << markovModel->getType() << " not expected."); } } From 35c9b58fda7970eefa99410f625070b7c590f124 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 12 Jun 2017 15:33:11 +0200 Subject: [PATCH 4/4] added a test case for SparseMatri::restrictRows and fixed it --- src/storm/storage/SparseMatrix.cpp | 37 +++++++------ src/test/storage/SparseMatrixTest.cpp | 78 +++++++++++++++++++++++++++ 2 files changed, 98 insertions(+), 17 deletions(-) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index b8f694939..99a716415 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -919,32 +919,35 @@ namespace storm { for (auto const& row : rowsToKeep) { entryCount += this->getRow(row).getNumberOfEntries(); } - + + // Get the smallest row group index such that all row groups with at least this index are empty. + uint_fast64_t firstTrailingEmptyRowGroup = this->getRowGroupCount(); + for (auto groupIndexIt = this->getRowGroupIndices().rbegin() + 1; groupIndexIt != this->getRowGroupIndices().rend(); ++groupIndexIt) { + if (rowsToKeep.getNextSetIndex(*groupIndexIt) != rowsToKeep.size()) { + break; + } + --firstTrailingEmptyRowGroup; + } + STORM_LOG_THROW(allowEmptyRowGroups || firstTrailingEmptyRowGroup == this->getRowGroupCount(), storm::exceptions::InvalidArgumentException, "Empty rows are not allowed, but row group " << firstTrailingEmptyRowGroup << " is empty."); + // build the matrix. The row grouping will always be considered as nontrivial. SparseMatrixBuilder builder(rowsToKeep.getNumberOfSetBits(), this->getColumnCount(), entryCount, true, true, this->getRowGroupCount()); uint_fast64_t newRow = 0; - for (uint_fast64_t rowGroup = 0; rowGroup < this->getRowGroupCount(); ++rowGroup) { + for (uint_fast64_t rowGroup = 0; rowGroup < firstTrailingEmptyRowGroup; ++rowGroup) { + // Add a new row group builder.newRowGroup(newRow); bool rowGroupEmpty = true; - if (this->hasTrivialRowGrouping()) { - if (rowsToKeep.get(rowGroup)) { - rowGroupEmpty = false; - for (auto const& entry : this->getRow(rowGroup)) { - builder.addNextValue(newRow, entry.getColumn(), entry.getValue()); - } - ++newRow; - } - } else { - for (uint_fast64_t row = rowsToKeep.getNextSetIndex(this->getRowGroupIndices()[rowGroup]); row < this->getRowGroupIndices()[rowGroup + 1]; row = rowsToKeep.getNextSetIndex(row + 1)) { - rowGroupEmpty = false; - for (auto const& entry: this->getRow(row)) { - builder.addNextValue(newRow, entry.getColumn(), entry.getValue()); - } - ++newRow; + for (uint_fast64_t row = rowsToKeep.getNextSetIndex(this->getRowGroupIndices()[rowGroup]); row < this->getRowGroupIndices()[rowGroup + 1]; row = rowsToKeep.getNextSetIndex(row + 1)) { + rowGroupEmpty = false; + for (auto const& entry: this->getRow(row)) { + builder.addNextValue(newRow, entry.getColumn(), entry.getValue()); } + ++newRow; } STORM_LOG_THROW(allowEmptyRowGroups || !rowGroupEmpty, storm::exceptions::InvalidArgumentException, "Empty rows are not allowed, but row group " << rowGroup << " is empty."); } + + // The all remaining row groups will be empty. Note that it is not allowed to call builder.addNewGroup(...) if there are no more rows afterwards. SparseMatrix res = builder.build(); return res; } diff --git a/src/test/storage/SparseMatrixTest.cpp b/src/test/storage/SparseMatrixTest.cpp index b331fefe1..1b468c318 100644 --- a/src/test/storage/SparseMatrixTest.cpp +++ b/src/test/storage/SparseMatrixTest.cpp @@ -3,6 +3,7 @@ #include "storm/storage/BitVector.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/OutOfRangeException.h" +#include "storm/exceptions/InvalidArgumentException.h" TEST(SparseMatrixBuilder, CreationWithDimensions) { storm::storage::SparseMatrixBuilder matrixBuilder(3, 4, 5); @@ -374,6 +375,83 @@ TEST(SparseMatrix, Submatrix) { ASSERT_TRUE(matrix4 == matrix5); } +TEST(SparseMatrix, RestrictRows) { + storm::storage::SparseMatrixBuilder matrixBuilder1(7, 4, 9, true, true, 3); + ASSERT_NO_THROW(matrixBuilder1.newRowGroup(0)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder1.newRowGroup(2)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder1.newRowGroup(4)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(6, 3, 0.3)); + storm::storage::SparseMatrix matrix1; + ASSERT_NO_THROW(matrix1 = matrixBuilder1.build()); + + storm::storage::BitVector constraint1(7); + constraint1.set(0); + constraint1.set(1); + constraint1.set(2); + constraint1.set(5); + + storm::storage::SparseMatrix matrix1Prime; + ASSERT_NO_THROW(matrix1Prime = matrix1.restrictRows(constraint1)); + + storm::storage::SparseMatrixBuilder matrixBuilder2(4, 4, 5, true, true, 3); + ASSERT_NO_THROW(matrixBuilder2.newRowGroup(0)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder2.newRowGroup(2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.newRowGroup(3)); + storm::storage::SparseMatrix matrix2; + ASSERT_NO_THROW(matrix2 = matrixBuilder2.build()); + + ASSERT_EQ(matrix2, matrix1Prime); + + storm::storage::BitVector constraint2(4); + constraint2.set(1); + constraint2.set(2); + + storm::storage::SparseMatrix matrix2Prime; + ASSERT_THROW(matrix2Prime = matrix2.restrictRows(constraint2), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(matrix2Prime = matrix2.restrictRows(constraint2, true)); + + storm::storage::SparseMatrixBuilder matrixBuilder3(2, 4, 3, true, true, 3); + ASSERT_NO_THROW(matrixBuilder3.newRowGroup(0)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(0, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(0, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder3.newRowGroup(1)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(1, 0, 0.5)); + storm::storage::SparseMatrix matrix3; + ASSERT_NO_THROW(matrix3 = matrixBuilder3.build()); + + ASSERT_EQ(matrix3, matrix2Prime); + + matrix3.makeRowGroupingTrivial(); + storm::storage::BitVector constraint3(2); + constraint3.set(1); + + storm::storage::SparseMatrix matrix3Prime; + ASSERT_THROW(matrix3Prime = matrix3.restrictRows(constraint3), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(matrix3Prime = matrix3.restrictRows(constraint3, true)); + + storm::storage::SparseMatrixBuilder matrixBuilder4(1, 4, 1, true, true, 2); + ASSERT_NO_THROW(matrixBuilder4.newRowGroup(0)); + ASSERT_NO_THROW(matrixBuilder4.newRowGroup(0)); + ASSERT_NO_THROW(matrixBuilder4.addNextValue(0, 0, 0.5)); + storm::storage::SparseMatrix matrix4; + ASSERT_NO_THROW(matrix4 = matrixBuilder4.build()); + + ASSERT_EQ(matrix4, matrix3Prime); +} + TEST(SparseMatrix, Transpose) { storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9); ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0));