From 017fa192815a56d2641cd1c15cd08068f0607a42 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 15 Feb 2016 11:55:42 +0100 Subject: [PATCH 1/2] Fixed compile issue Former-commit-id: a58c76d17584b72fcb4c04313f3168ffef854975 --- src/solver/stateelimination/StateEliminator.cpp | 3 +-- src/solver/stateelimination/StateEliminator.h | 5 ++++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/solver/stateelimination/StateEliminator.cpp b/src/solver/stateelimination/StateEliminator.cpp index 3e3d8c53a..01dc8a5af 100644 --- a/src/solver/stateelimination/StateEliminator.cpp +++ b/src/solver/stateelimination/StateEliminator.cpp @@ -1,7 +1,6 @@ #include "src/solver/stateelimination/StateEliminator.h" #include "src/storage/BitVector.h" -#include "src/adapters/CarlAdapter.h" #include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidStateException.h" @@ -256,4 +255,4 @@ namespace storm { } // namespace stateelimination } // namespace storage -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/solver/stateelimination/StateEliminator.h b/src/solver/stateelimination/StateEliminator.h index 2a58912e8..a0bf04a98 100644 --- a/src/solver/stateelimination/StateEliminator.h +++ b/src/solver/stateelimination/StateEliminator.h @@ -4,6 +4,9 @@ #include "src/storage/FlexibleSparseMatrix.h" #include "src/storage/SparseMatrix.h" #include "src/storage/sparse/StateType.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/StandardRewardModel.h" +#include "src/adapters/CarlAdapter.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" namespace storm { @@ -39,4 +42,4 @@ namespace storm { } // namespace storage } // namespace storm -#endif // STORM_SOLVER_STATEELIMINATION_STATEELIMINATOR_H_ \ No newline at end of file +#endif // STORM_SOLVER_STATEELIMINATION_STATEELIMINATOR_H_ From 3d4c5b3df289d0431000fd9acadaa98aba06a91f Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 15 Feb 2016 17:06:16 +0100 Subject: [PATCH 2/2] Fixed output for flexible matrix Former-commit-id: e2c9913b6eddb4d5add820623115a0fa21a2cb54 --- src/storage/FlexibleSparseMatrix.cpp | 77 ++++++++++++++++++---------- src/storage/FlexibleSparseMatrix.h | 15 ++++++ 2 files changed, 65 insertions(+), 27 deletions(-) diff --git a/src/storage/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp index 99ed68337..03fcf3d57 100644 --- a/src/storage/FlexibleSparseMatrix.cpp +++ b/src/storage/FlexibleSparseMatrix.cpp @@ -63,6 +63,11 @@ namespace storm { return getRow(rowGroupIndices[rowGroup] + offset); } + template + std::vector::index_type> const& FlexibleSparseMatrix::getRowGroupIndices() const { + return rowGroupIndices; + } + template typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getRowCount() const { return this->data.size(); @@ -164,49 +169,64 @@ namespace storm { } return false; } + + template + std::ostream& FlexibleSparseMatrix::printRow(std::ostream& out, index_type const& rowIndex) const { + index_type columnIndex = 0; + row_type row = this->getRow(rowIndex); + for (index_type column = 0; column < this->getColumnCount(); ++column) { + if (columnIndex < row.size() && row[columnIndex].getColumn() == column) { + // Insert entry + out << row[columnIndex].getValue() << "\t"; + ++columnIndex; + } else { + // Insert zero + out << "0\t"; + } + } + return out; + } + template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix) { + typedef typename FlexibleSparseMatrix::index_type FlexibleIndex; + // Print column numbers in header. out << "\t\t"; - for (typename FlexibleSparseMatrix::index_type i = 0; i < matrix.getColumnCount(); ++i) { + for (FlexibleIndex i = 0; i < matrix.getColumnCount(); ++i) { out << i << "\t"; } out << std::endl; - typename FlexibleSparseMatrix::index_type endIndex = matrix.hasNontrivialRowGrouping() ? matrix.getRowGroupCount() : matrix.getRowCount(); - // Iterate over all rows. - for (typename SparseMatrix::index_type i = 0; i < endIndex; ++i) { - if (matrix.hasNontrivialRowGrouping()) { - out << "\t---- group " << i << "/" << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl; + if (matrix.hasNontrivialRowGrouping()) { + // Iterate over all row groups + FlexibleIndex rowGroupCount = matrix.getRowGroupCount(); + for (FlexibleIndex rowGroup = 0; rowGroup < rowGroupCount; ++rowGroup) { + out << "\t---- group " << rowGroup << "/" << (rowGroupCount - 1) << " ---- " << std::endl; + FlexibleIndex endRow = rowGroup+1 < rowGroupCount ? matrix.rowGroupIndices[rowGroup + 1] : matrix.getRowCount(); + // Iterate over all rows. + for (FlexibleIndex row = matrix.rowGroupIndices[rowGroup]; row < endRow; ++row) { + // Print the actual row. + out << rowGroup << "\t(\t"; + matrix.printRow(out, row); + out << "\t)\t" << rowGroup << std::endl; + } } - typename FlexibleSparseMatrix::index_type startRow = matrix.hasNontrivialRowGrouping() ? matrix.rowGroupIndices[i] : i; - typename FlexibleSparseMatrix::index_type endRow = matrix.hasNontrivialRowGrouping() ? matrix.rowGroupIndices[i + 1] : i+1; - for (typename FlexibleSparseMatrix::index_type rowIndex = startRow; rowIndex < endRow; ++rowIndex) { + + } else { + // Iterate over all rows + for (FlexibleIndex row = 0; row < matrix.getRowCount(); ++row) { // Print the actual row. - out << i << "\t(\t"; - typename FlexibleSparseMatrix::row_type row = matrix.getRow(rowIndex); - typename FlexibleSparseMatrix::index_type columnIndex = 0; - for (auto const& entry : row) { - //Insert zero between entries. - while (columnIndex < entry.getColumn()) { - out << "0\t"; - ++columnIndex; - } - ++columnIndex; - out << entry.getValue() << "\t"; - } - //Insert remaining zeros. - while (columnIndex++ <= matrix.getColumnCount()) { - out << "0\t"; - } - out << "\t)\t" << i << std::endl; + out << row << "\t(\t"; + matrix.printRow(out, row); + out << "\t)\t" << row << std::endl; } } // Print column numbers in footer. out << "\t\t"; - for (typename FlexibleSparseMatrix::index_type i = 0; i < matrix.getColumnCount(); ++i) { + for (FlexibleIndex i = 0; i < matrix.getColumnCount(); ++i) { out << i << "\t"; } out << std::endl; @@ -215,8 +235,11 @@ namespace storm { // Explicitly instantiate the matrix. template class FlexibleSparseMatrix; + template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix); + #ifdef STORM_HAVE_CARL template class FlexibleSparseMatrix; + template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix); #endif } // namespace storage diff --git a/src/storage/FlexibleSparseMatrix.h b/src/storage/FlexibleSparseMatrix.h index 163a25aa4..d7e74f062 100644 --- a/src/storage/FlexibleSparseMatrix.h +++ b/src/storage/FlexibleSparseMatrix.h @@ -85,6 +85,13 @@ namespace storm { * @return An object representing the given row. */ row_type const& getRow(index_type rowGroup, index_type entryInGroup) const; + + /*! + * Returns the grouping of rows of this matrix. + * + * @return The grouping of rows of this matrix. + */ + std::vector const& getRowGroupIndices() const; /*! * Returns the number of rows of the matrix. @@ -163,6 +170,14 @@ namespace storm { */ bool rowHasDiagonalElement(storm::storage::sparse::state_type state); + /*! + * Print row. + * @param out Output stream. + * @param rowIndex Index of row to print. + * @return Output with printed row. + */ + std::ostream& printRow(std::ostream& out, index_type const& rowIndex) const; + template friend std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix);