sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Started to pimp matrix. First step: added proper methods setColumn/setValue that operate on a matrix entry and removed the non-const versions of getColumn/getValue. Added a typedef for the index type in the matrix so that it becomes possible to have matrices with a different index type (e.g. 32-bit values). 

Former-commit-id: 3cc0fdf9ee
main
dehnert 11 years ago
parent
01cefbb2c0
commit
ab58103555
7 changed files with 362 additions and 335 deletions
Unified View
  1. 6
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  2. 2
      src/models/MarkovAutomaton.h
  3. 492
      src/storage/SparseMatrix.cpp
  4. 185
      src/storage/SparseMatrix.h
  5. 8
      src/storage/dd/CuddDd.cpp
  6. 2
      src/storage/dd/CuddDd.h
  7. 2
      test/functional/storage/SparseMatrixTest.cpp

6
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
View File

@ -149,9 +149,9 @@ namespace storm {
for (auto& element : aMarkovian.getRow(rowIndex)) { for (auto& element : aMarkovian.getRow(rowIndex)) {
ValueType eTerm = std::exp(-exitRates[state] * delta); ValueType eTerm = std::exp(-exitRates[state] * delta);
if (element.getColumn() == rowIndex) { if (element.getColumn() == rowIndex) {
element.getValue() = (storm::utility::constantOne<ValueType>() - eTerm) * element.getValue() + eTerm; element.setValue((storm::utility::constantOne<ValueType>() - eTerm) * element.getValue() + eTerm);
} else { } else {
element.getValue() = (storm::utility::constantOne<ValueType>() - eTerm) * element.getValue(); element.setValue((storm::utility::constantOne<ValueType>() - eTerm) * element.getValue());
} }
} }
++rowIndex; ++rowIndex;
@ -161,7 +161,7 @@ namespace storm {
rowIndex = 0; rowIndex = 0;
for (auto state : markovianNonGoalStates) { for (auto state : markovianNonGoalStates) {
for (auto& element : aMarkovianToProbabilistic.getRow(rowIndex)) { for (auto& element : aMarkovianToProbabilistic.getRow(rowIndex)) {
element.getValue() = (1 - std::exp(-exitRates[state] * delta)) * element.getValue(); element.setValue((1 - std::exp(-exitRates[state] * delta)) * element.getValue());
} }
++rowIndex; ++rowIndex;
} }

2
src/models/MarkovAutomaton.h
View File

@ -259,7 +259,7 @@ namespace storm {
void turnRatesToProbabilities() { void turnRatesToProbabilities() {
for (auto state : this->markovianStates) { for (auto state : this->markovianStates) {
for (auto& transition : this->transitionMatrix.getRowGroup(state)) { for (auto& transition : this->transitionMatrix.getRowGroup(state)) {
transition.getValue() /= this->exitRates[state]; transition.setValue(transition.getValue() / this->exitRates[state]);
} }
} }
} }

492
src/storage/SparseMatrix.cpp
File diff suppressed because it is too large
View File

185
src/storage/SparseMatrix.h
View File

@ -30,7 +30,7 @@ namespace storm {
// Forward declare matrix class. // Forward declare matrix class.
template<typename T> class SparseMatrix; template<typename T> class SparseMatrix;
template<typename T> template<typename IndexType, typename ValueType>
class MatrixEntry { class MatrixEntry {
public: public:
/*! /*!
@ -39,14 +39,14 @@ namespace storm {
* @param column The column of the matrix entry. * @param column The column of the matrix entry.
* @param value The value of the matrix entry. * @param value The value of the matrix entry.
*/ */
MatrixEntry(uint_fast64_t column, T value); MatrixEntry(IndexType column, ValueType value);
/*! /*!
* Move-constructs the matrix entry fro the given column-value pair. * Move-constructs the matrix entry fro the given column-value pair.
* *
* @param pair The column-value pair from which to move-construct the matrix entry. * @param pair The column-value pair from which to move-construct the matrix entry.
*/ */
MatrixEntry(std::pair<uint_fast64_t, T>&& pair); MatrixEntry(std::pair<IndexType, ValueType>&& pair);
MatrixEntry() = default; MatrixEntry() = default;
MatrixEntry(MatrixEntry const& other) = default; MatrixEntry(MatrixEntry const& other) = default;
@ -61,46 +61,46 @@ namespace storm {
* *
* @return The column of the matrix entry. * @return The column of the matrix entry.
*/ */
uint_fast64_t const& getColumn() const; IndexType const& getColumn() const;
/*! /*!
* Retrieves the column of the matrix entry. * Sets the column of the current entry.
* *
* @return The column of the matrix entry. * @param column The column to set for this entry.
*/ */
uint_fast64_t& getColumn(); void setColumn(IndexType const& column);
/*! /*!
* Retrieves the value of the matrix entry. * Retrieves the value of the matrix entry.
* *
* @return The value of the matrix entry. * @return The value of the matrix entry.
*/ */
T const& getValue() const; ValueType const& getValue() const;
/*! /*!
* Retrieves the value of the matrix entry. * Sets the value of the entry in the matrix.
* *
* @return The value of the matrix entry. * @param value The value that is to be set for this entry.
*/ */
T& getValue(); void setValue(ValueType const& value);
/*! /*!
* Retrieves a pair of column and value that characterizes this entry. * Retrieves a pair of column and value that characterizes this entry.
* *
* @return A column-value pair that characterizes this entry. * @return A column-value pair that characterizes this entry.
*/ */
std::pair<uint_fast64_t, T> const& getColumnValuePair() const; std::pair<IndexType, ValueType> const& getColumnValuePair() const;
private: private:
// The actual matrix entry. // The actual matrix entry.
std::pair<uint_fast64_t, T> entry; std::pair<IndexType, ValueType> entry;
}; };
/*! /*!
* Computes the hash value of a matrix entry. * Computes the hash value of a matrix entry.
*/ */
template<typename T> template<typename IndexType, typename ValueType>
std::size_t hash_value(MatrixEntry<T> const& matrixEntry) { std::size_t hash_value(MatrixEntry<IndexType, ValueType> const& matrixEntry) {
std::size_t seed = 0; std::size_t seed = 0;
boost::hash_combine(seed, matrixEntry.getColumn()); boost::hash_combine(seed, matrixEntry.getColumn());
boost::hash_combine(seed, matrixEntry.getValue()); boost::hash_combine(seed, matrixEntry.getValue());
@ -110,9 +110,11 @@ namespace storm {
/*! /*!
* A class that can be used to build a sparse matrix by adding value by value. * A class that can be used to build a sparse matrix by adding value by value.
*/ */
template<typename T> template<typename ValueType>
class SparseMatrixBuilder { class SparseMatrixBuilder {
public: public:
typedef uint_fast64_t IndexType;
/*! /*!
* Constructs a sparse matrix builder producing a matrix with the given number of rows, columns and entries. * Constructs a sparse matrix builder producing a matrix with the given number of rows, columns and entries.
* *
@ -124,7 +126,7 @@ namespace storm {
* @param rowGroups The number of row groups of the resulting matrix. This is only relevant if the matrix * @param rowGroups The number of row groups of the resulting matrix. This is only relevant if the matrix
* has a custom row grouping. * has a custom row grouping.
*/ */
SparseMatrixBuilder(uint_fast64_t rows = 0, uint_fast64_t columns = 0, uint_fast64_t entries = 0, bool hasCustomRowGrouping = false, uint_fast64_t rowGroups = 0); SparseMatrixBuilder(IndexType rows = 0, IndexType columns = 0, IndexType entries = 0, bool hasCustomRowGrouping = false, IndexType rowGroups = 0);
/*! /*!
* Sets the matrix entry at the given row and column to the given value. After all entries have been added, * Sets the matrix entry at the given row and column to the given value. After all entries have been added,
@ -139,7 +141,7 @@ namespace storm {
* @param column The column in which the matrix entry is to be set. * @param column The column in which the matrix entry is to be set.
* @param value The value that is to be set at the specified row and column. * @param value The value that is to be set at the specified row and column.
*/ */
void addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value); void addNextValue(IndexType row, IndexType column, ValueType const& value);
/*! /*!
* Starts a new row group in the matrix. Note that this needs to be called before any entries in the new row * Starts a new row group in the matrix. Note that this needs to be called before any entries in the new row
@ -147,7 +149,7 @@ namespace storm {
* *
* @param startingRow The starting row of the new row group. * @param startingRow The starting row of the new row group.
*/ */
void newRowGroup(uint_fast64_t startingRow); void newRowGroup(IndexType startingRow);
/* /*
* Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix * Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix
@ -168,7 +170,7 @@ namespace storm {
* effect if the matrix has been created without the number of row groups given. By construction, the row * effect if the matrix has been created without the number of row groups given. By construction, the row
* groups added this way will be empty. * groups added this way will be empty.
*/ */
SparseMatrix<T> build(uint_fast64_t overriddenRowCount = 0, uint_fast64_t overriddenColumnCount = 0, uint_fast64_t overriddenRowGroupCount = 0); SparseMatrix<ValueType> build(IndexType overriddenRowCount = 0, IndexType overriddenColumnCount = 0, IndexType overriddenRowGroupCount = 0);
private: private:
/*! /*!
@ -182,16 +184,16 @@ namespace storm {
bool rowCountSet; bool rowCountSet;
// The number of rows of the matrix. // The number of rows of the matrix.
uint_fast64_t rowCount; IndexType rowCount;
// A flag indicating whether the number of columns was set upon construction. // A flag indicating whether the number of columns was set upon construction.
bool columnCountSet; bool columnCountSet;
// The number of columns of the matrix. // The number of columns of the matrix.
uint_fast64_t columnCount; IndexType columnCount;
// The number of entries in the matrix. // The number of entries in the matrix.
uint_fast64_t entryCount; IndexType entryCount;
// A flag indicating whether the builder is to construct a custom row grouping for the matrix. // A flag indicating whether the builder is to construct a custom row grouping for the matrix.
bool hasCustomRowGrouping; bool hasCustomRowGrouping;
@ -200,37 +202,37 @@ namespace storm {
bool rowGroupCountSet; bool rowGroupCountSet;
// The number of row groups in the matrix. // The number of row groups in the matrix.
uint_fast64_t rowGroupCount; IndexType rowGroupCount;
std::vector<uint_fast64_t> rowGroupIndices; std::vector<IndexType> rowGroupIndices;
// Stores whether the storage of the matrix was preallocated or not. // Stores whether the storage of the matrix was preallocated or not.
bool storagePreallocated; bool storagePreallocated;
// The storage for the columns and values of all entries in the matrix. // The storage for the columns and values of all entries in the matrix.
std::vector<MatrixEntry<T>> columnsAndValues; std::vector<MatrixEntry<IndexType, ValueType>> columnsAndValues;
// A vector containing the indices at which each given row begins. This index is to be interpreted as an // A vector containing the indices at which each given row begins. This index is to be interpreted as an
// index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries
// in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last
// entry is not included anymore. // entry is not included anymore.
std::vector<uint_fast64_t> rowIndications; std::vector<IndexType> rowIndications;
// Stores the current number of entries in the matrix. This is used for inserting an entry into a matrix // Stores the current number of entries in the matrix. This is used for inserting an entry into a matrix
// with preallocated storage. // with preallocated storage.
uint_fast64_t currentEntryCount; IndexType currentEntryCount;
// Stores the row of the last entry in the matrix. This is used for correctly inserting an entry into a // Stores the row of the last entry in the matrix. This is used for correctly inserting an entry into a
// matrix. // matrix.
uint_fast64_t lastRow; IndexType lastRow;
// Stores the column of the currently last entry in the matrix. This is used for correctly inserting an // Stores the column of the currently last entry in the matrix. This is used for correctly inserting an
// entry into a matrix. // entry into a matrix.
uint_fast64_t lastColumn; IndexType lastColumn;
// Stores the currently active row group. This is used for correctly constructing the row grouping of the // Stores the currently active row group. This is used for correctly constructing the row grouping of the
// matrix. // matrix.
uint_fast64_t currentRowGroup; IndexType currentRowGroup;
}; };
/*! /*!
@ -247,7 +249,7 @@ namespace storm {
* It should be observed that due to the nature of the sparse matrix format, entries can only be inserted in * It should be observed that due to the nature of the sparse matrix format, entries can only be inserted in
* order, i.e. row by row and column by column. * order, i.e. row by row and column by column.
*/ */
template<typename T> template<typename ValueType>
class SparseMatrix { class SparseMatrix {
public: public:
// Declare adapter classes as friends to use internal data. // Declare adapter classes as friends to use internal data.
@ -255,8 +257,9 @@ namespace storm {
friend class storm::adapters::EigenAdapter; friend class storm::adapters::EigenAdapter;
friend class storm::adapters::StormAdapter; friend class storm::adapters::StormAdapter;
typedef typename std::vector<MatrixEntry<T>>::iterator iterator; typedef uint_fast64_t IndexType;
typedef typename std::vector<MatrixEntry<T>>::const_iterator const_iterator; typedef typename std::vector<MatrixEntry<IndexType, ValueType>>::iterator iterator;
typedef typename std::vector<MatrixEntry<IndexType, ValueType>>::const_iterator const_iterator;
/*! /*!
* This class represents a number of consecutive rows of the matrix. * This class represents a number of consecutive rows of the matrix.
@ -270,7 +273,7 @@ namespace storm {
* @param begin An iterator that points to the beginning of the row. * @param begin An iterator that points to the beginning of the row.
* @param entryCount The number of entrys in the rows. * @param entryCount The number of entrys in the rows.
*/ */
rows(iterator begin, uint_fast64_t entryCount); rows(iterator begin, IndexType entryCount);
/*! /*!
* Retrieves an iterator that points to the beginning of the rows. * Retrieves an iterator that points to the beginning of the rows.
@ -286,12 +289,19 @@ namespace storm {
*/ */
iterator end(); iterator end();
/*!
* Retrieves the number of entries in the rows.
*
* @return The number of entries in the rows.
*/
IndexType getNumberOfEntries() const;
private: private:
// The pointer to the columnd and value of the first entry. // The pointer to the columnd and value of the first entry.
iterator beginIterator; iterator beginIterator;
// The number of non-zero entries in the rows. // The number of non-zero entries in the rows.
uint_fast64_t entryCount; IndexType entryCount;
}; };
/*! /*!
@ -306,7 +316,7 @@ namespace storm {
* @param begin An iterator that points to the beginning of the row. * @param begin An iterator that points to the beginning of the row.
* @param entryCount The number of entrys in the rows. * @param entryCount The number of entrys in the rows.
*/ */
const_rows(const_iterator begin, uint_fast64_t entryCount); const_rows(const_iterator begin, IndexType entryCount);
/*! /*!
* Retrieves an iterator that points to the beginning of the rows. * Retrieves an iterator that points to the beginning of the rows.
@ -322,12 +332,19 @@ namespace storm {
*/ */
const_iterator end() const; const_iterator end() const;
/*!
* Retrieves the number of entries in the rows.
*
* @return The number of entries in the rows.
*/
IndexType getNumberOfEntries() const;
private: private:
// The pointer to the columnd and value of the first entry. // The pointer to the columnd and value of the first entry.
const_iterator beginIterator; const_iterator beginIterator;
// The number of non-zero entries in the rows. // The number of non-zero entries in the rows.
uint_fast64_t entryCount; IndexType entryCount;
}; };
/*! /*!
@ -347,14 +364,14 @@ namespace storm {
* *
* @param other The matrix from which to copy the content. * @param other The matrix from which to copy the content.
*/ */
SparseMatrix(SparseMatrix<T> const& other); SparseMatrix(SparseMatrix<ValueType> const& other);
/*! /*!
* Constructs a sparse matrix by moving the contents of the given matrix to the newly created one. * Constructs a sparse matrix by moving the contents of the given matrix to the newly created one.
* *
* @param other The matrix from which to move the content. * @param other The matrix from which to move the content.
*/ */
SparseMatrix(SparseMatrix<T>&& other); SparseMatrix(SparseMatrix<ValueType>&& other);
/*! /*!
* Constructs a sparse matrix by copying the given contents. * Constructs a sparse matrix by copying the given contents.
@ -364,7 +381,7 @@ namespace storm {
* @param columnsAndValues The vector containing the columns and values of the entries in the matrix. * @param columnsAndValues The vector containing the columns and values of the entries in the matrix.
* @param rowGroupIndices The vector representing the row groups in the matrix. * @param rowGroupIndices The vector representing the row groups in the matrix.
*/ */
SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<MatrixEntry<T>> const& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupIndices); SparseMatrix(IndexType columnCount, std::vector<IndexType> const& rowIndications, std::vector<MatrixEntry<IndexType, ValueType>> const& columnsAndValues, std::vector<IndexType> const& rowGroupIndices);
/*! /*!
* Constructs a sparse matrix by moving the given contents. * Constructs a sparse matrix by moving the given contents.
@ -374,21 +391,21 @@ namespace storm {
* @param columnsAndValues The vector containing the columns and values of the entries in the matrix. * @param columnsAndValues The vector containing the columns and values of the entries in the matrix.
* @param rowGroupIndices The vector representing the row groups in the matrix. * @param rowGroupIndices The vector representing the row groups in the matrix.
*/ */
SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<MatrixEntry<T>>&& columnsAndValues, std::vector<uint_fast64_t>&& rowGroupIndices); SparseMatrix(IndexType columnCount, std::vector<IndexType>&& rowIndications, std::vector<MatrixEntry<IndexType, ValueType>>&& columnsAndValues, std::vector<IndexType>&& rowGroupIndices);
/*! /*!
* Assigns the contents of the given matrix to the current one by deep-copying its contents. * Assigns the contents of the given matrix to the current one by deep-copying its contents.
* *
* @param other The matrix from which to copy-assign. * @param other The matrix from which to copy-assign.
*/ */
SparseMatrix<T>& operator=(SparseMatrix<T> const& other); SparseMatrix<ValueType>& operator=(SparseMatrix<ValueType> const& other);
/*! /*!
* Assigns the contents of the given matrix to the current one by moving its contents. * Assigns the contents of the given matrix to the current one by moving its contents.
* *
* @param other The matrix from which to move to contents. * @param other The matrix from which to move to contents.
*/ */
SparseMatrix<T>& operator=(SparseMatrix<T>&& other); SparseMatrix<ValueType>& operator=(SparseMatrix<ValueType>&& other);
/*! /*!
* Determines whether the current and the given matrix are semantically equal. * Determines whether the current and the given matrix are semantically equal.
@ -396,42 +413,42 @@ namespace storm {
* @param other The matrix with which to compare the current matrix. * @param other The matrix with which to compare the current matrix.
* @return True iff the given matrix is semantically equal to the current one. * @return True iff the given matrix is semantically equal to the current one.
*/ */
bool operator==(SparseMatrix<T> const& other) const; bool operator==(SparseMatrix<ValueType> const& other) const;
/*! /*!
* Returns the number of rows of the matrix. * Returns the number of rows of the matrix.
* *
* @return The number of rows of the matrix. * @return The number of rows of the matrix.
*/ */
uint_fast64_t getRowCount() const; IndexType getRowCount() const;
/*! /*!
* Returns the number of columns of the matrix. * Returns the number of columns of the matrix.
* *
* @return The number of columns of the matrix. * @return The number of columns of the matrix.
*/ */
uint_fast64_t getColumnCount() const; IndexType getColumnCount() const;
/*! /*!
* Returns the number of entries in the matrix. * Returns the number of entries in the matrix.
* *
* @return The number of entries in the matrix. * @return The number of entries in the matrix.
*/ */
uint_fast64_t getEntryCount() const; IndexType getEntryCount() const;
/*! /*!
* Returns the number of nonzero entries in the matrix. * Returns the number of nonzero entries in the matrix.
* *
* @return The number of nonzero entries in the matrix. * @return The number of nonzero entries in the matrix.
*/ */
uint_fast64_t getNonzeroEntryCount() const; IndexType getNonzeroEntryCount() const;
/*! /*!
* Returns the number of row groups in the matrix. * Returns the number of row groups in the matrix.
* *
* @return The number of row groups in the matrix. * @return The number of row groups in the matrix.
*/ */
uint_fast64_t getRowGroupCount() const; IndexType getRowGroupCount() const;
/*! /*!
* Returns the size of the given row group. * Returns the size of the given row group.
@ -439,14 +456,14 @@ namespace storm {
* @param group The group whose size to retrieve. * @param group The group whose size to retrieve.
* @return The number of rows that belong to the given row group. * @return The number of rows that belong to the given row group.
*/ */
uint_fast64_t getRowGroupSize(uint_fast64_t group) const; IndexType getRowGroupSize(IndexType group) const;
/*! /*!
* Returns the grouping of rows of this matrix. * Returns the grouping of rows of this matrix.
* *
* @return The grouping of rows of this matrix. * @return The grouping of rows of this matrix.
*/ */
std::vector<uint_fast64_t> const& getRowGroupIndices() const; std::vector<IndexType> const& getRowGroupIndices() const;
/*! /*!
* This function makes the given rows absorbing. * This function makes the given rows absorbing.
@ -469,7 +486,7 @@ namespace storm {
* @param row The row to be made Dirac. * @param row The row to be made Dirac.
* @param column The index of the column whose value is to be set to 1. * @param column The index of the column whose value is to be set to 1.
*/ */
void makeRowDirac(const uint_fast64_t row, const uint_fast64_t column); void makeRowDirac(const IndexType row, const IndexType column);
/* /*
* Sums the entries in the given row and columns. * Sums the entries in the given row and columns.
@ -478,7 +495,7 @@ namespace storm {
* @param columns A bit vector that indicates which columns to add. * @param columns A bit vector that indicates which columns to add.
* @return The sum of the entries in the given row and columns. * @return The sum of the entries in the given row and columns.
*/ */
T getConstrainedRowSum(uint_fast64_t row, storm::storage::BitVector const& columns) const; ValueType getConstrainedRowSum(IndexType row, storm::storage::BitVector const& columns) const;
/*! /*!
* Computes a vector whose i-th entry is the sum of the entries in the i-th selected row where only those * Computes a vector whose i-th entry is the sum of the entries in the i-th selected row where only those
@ -489,7 +506,7 @@ namespace storm {
* *
* @return A vector whose elements are the sums of the selected columns in each row. * @return A vector whose elements are the sums of the selected columns in each row.
*/ */
std::vector<T> getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const; std::vector<ValueType> getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const;
/*! /*!
* Computes a vector whose entries represent the sums of selected columns for all rows in selected row * Computes a vector whose entries represent the sums of selected columns for all rows in selected row
@ -500,7 +517,7 @@ namespace storm {
* @return A vector whose entries represent the sums of selected columns for all rows in selected row * @return A vector whose entries represent the sums of selected columns for all rows in selected row
* groups. * groups.
*/ */
std::vector<T> getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const; std::vector<ValueType> getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const;
/*! /*!
* Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not * Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not
@ -524,7 +541,7 @@ namespace storm {
* each row in row group i. This can then be used for inserting other values later. * each row in row group i. This can then be used for inserting other values later.
* @return A submatrix of the current matrix by selecting one row out of each row group. * @return A submatrix of the current matrix by selecting one row out of each row group.
*/ */
SparseMatrix selectRowsFromRowGroups(std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const; SparseMatrix selectRowsFromRowGroups(std::vector<IndexType> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const;
/*! /*!
* Transposes the matrix. * Transposes the matrix.
@ -533,7 +550,7 @@ namespace storm {
* *
* @return A sparse matrix that represents the transpose of this matrix. * @return A sparse matrix that represents the transpose of this matrix.
*/ */
storm::storage::SparseMatrix<T> transpose(bool joinGroups = false) const; storm::storage::SparseMatrix<ValueType> transpose(bool joinGroups = false) const;
/*! /*!
* Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A). * Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A).
@ -561,7 +578,7 @@ namespace storm {
* *
* @return A pair (L+U, D^-1) containing the matrix L+U and the inverted diagonal matrix D^-1. * @return A pair (L+U, D^-1) containing the matrix L+U and the inverted diagonal matrix D^-1.
*/ */
std::pair<storm::storage::SparseMatrix<T>, storm::storage::SparseMatrix<T>> getJacobiDecomposition() const; std::pair<storm::storage::SparseMatrix<ValueType>, storm::storage::SparseMatrix<ValueType>> getJacobiDecomposition() const;
/*! /*!
* Performs a pointwise matrix multiplication of the matrix with the given matrix and returns a vector * Performs a pointwise matrix multiplication of the matrix with the given matrix and returns a vector
@ -573,7 +590,7 @@ namespace storm {
* @return A vector containing the sum of the entries in each row of the matrix resulting from pointwise * @return A vector containing the sum of the entries in each row of the matrix resulting from pointwise
* multiplication of the current matrix with the given matrix. * multiplication of the current matrix with the given matrix.
*/ */
std::vector<T> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<T> const& otherMatrix) const; std::vector<ValueType> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<ValueType> const& otherMatrix) const;
/*! /*!
* Multiplies the matrix with the given vector and writes the result to the given result vector. If a * Multiplies the matrix with the given vector and writes the result to the given result vector. If a
@ -584,7 +601,7 @@ namespace storm {
* @param result The vector that is supposed to hold the result of the multiplication after the operation. * @param result The vector that is supposed to hold the result of the multiplication after the operation.
* @return The product of the matrix and the given vector as the content of the given result vector. * @return The product of the matrix and the given vector as the content of the given result vector.
*/ */
void multiplyWithVector(std::vector<T> const& vector, std::vector<T>& result) const; void multiplyWithVector(std::vector<ValueType> const& vector, std::vector<ValueType>& result) const;
/*! /*!
* Multiplies the matrix with the given vector in a sequential way and writes the result to the given result * Multiplies the matrix with the given vector in a sequential way and writes the result to the given result
@ -594,7 +611,7 @@ namespace storm {
* @param result The vector that is supposed to hold the result of the multiplication after the operation. * @param result The vector that is supposed to hold the result of the multiplication after the operation.
* @return The product of the matrix and the given vector as the content of the given result vector. * @return The product of the matrix and the given vector as the content of the given result vector.
*/ */
void multiplyWithVectorSequential(std::vector<T> const& vector, std::vector<T>& result) const; void multiplyWithVectorSequential(std::vector<ValueType> const& vector, std::vector<ValueType>& result) const;
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
/*! /*!
@ -605,7 +622,7 @@ namespace storm {
* @param result The vector that is supposed to hold the result of the multiplication after the operation. * @param result The vector that is supposed to hold the result of the multiplication after the operation.
* @return The product of the matrix and the given vector as the content of the given result vector. * @return The product of the matrix and the given vector as the content of the given result vector.
*/ */
void multiplyWithVectorParallel(std::vector<T> const& vector, std::vector<T>& result) const; void multiplyWithVectorParallel(std::vector<ValueType> const& vector, std::vector<ValueType>& result) const;
#endif #endif
/*! /*!
@ -614,7 +631,7 @@ namespace storm {
* @param row The row that is to be summed. * @param row The row that is to be summed.
* @return The sum of the selected row. * @return The sum of the selected row.
*/ */
T getRowSum(uint_fast64_t row) const; ValueType getRowSum(IndexType row) const;
/*! /*!
* Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a submatrix * Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a submatrix
@ -623,7 +640,7 @@ namespace storm {
* @param matrix The matrix that possibly is a supermatrix of the current matrix. * @param matrix The matrix that possibly is a supermatrix of the current matrix.
* @return True iff the current matrix is a submatrix of the given matrix. * @return True iff the current matrix is a submatrix of the given matrix.
*/ */
bool isSubmatrixOf(SparseMatrix<T> const& matrix) const; bool isSubmatrixOf(SparseMatrix<ValueType> const& matrix) const;
template<typename TPrime> template<typename TPrime>
friend std::ostream& operator<<(std::ostream& out, SparseMatrix<TPrime> const& matrix); friend std::ostream& operator<<(std::ostream& out, SparseMatrix<TPrime> const& matrix);
@ -649,7 +666,7 @@ namespace storm {
* @param endRow The ending row (which is included in the result). * @param endRow The ending row (which is included in the result).
* @return An object representing the consecutive rows given by the parameters. * @return An object representing the consecutive rows given by the parameters.
*/ */
const_rows getRows(uint_fast64_t startRow, uint_fast64_t endRow) const; const_rows getRows(IndexType startRow, IndexType endRow) const;
/*! /*!
* Returns an object representing the consecutive rows given by the parameters. * Returns an object representing the consecutive rows given by the parameters.
@ -658,7 +675,7 @@ namespace storm {
* @param endRow The ending row (which is included in the result). * @param endRow The ending row (which is included in the result).
* @return An object representing the consecutive rows given by the parameters. * @return An object representing the consecutive rows given by the parameters.
*/ */
rows getRows(uint_fast64_t startRow, uint_fast64_t endRow); rows getRows(IndexType startRow, IndexType endRow);
/*! /*!
* Returns an object representing the given row. * Returns an object representing the given row.
@ -666,7 +683,7 @@ namespace storm {
* @param row The row to get. * @param row The row to get.
* @return An object representing the given row. * @return An object representing the given row.
*/ */
const_rows getRow(uint_fast64_t row) const; const_rows getRow(IndexType row) const;
/*! /*!
* Returns an object representing the given row. * Returns an object representing the given row.
@ -674,7 +691,7 @@ namespace storm {
* @param row The row to get. * @param row The row to get.
* @return An object representing the given row. * @return An object representing the given row.
*/ */
rows getRow(uint_fast64_t row); rows getRow(IndexType row);
/*! /*!
* Returns an object representing the given row group. * Returns an object representing the given row group.
@ -682,7 +699,7 @@ namespace storm {
* @param rowGroup The row group to get. * @param rowGroup The row group to get.
* @return An object representing the given row group. * @return An object representing the given row group.
*/ */
const_rows getRowGroup(uint_fast64_t rowGroup) const; const_rows getRowGroup(IndexType rowGroup) const;
/*! /*!
* Returns an object representing the given row group. * Returns an object representing the given row group.
@ -690,7 +707,7 @@ namespace storm {
* @param rowGroup The row group to get. * @param rowGroup The row group to get.
* @return An object representing the given row group. * @return An object representing the given row group.
*/ */
rows getRowGroup(uint_fast64_t rowGroup); rows getRowGroup(IndexType rowGroup);
/*! /*!
* Retrieves an iterator that points to the beginning of the given row. * Retrieves an iterator that points to the beginning of the given row.
@ -698,7 +715,7 @@ namespace storm {
* @param row The row to the beginning of which the iterator has to point. * @param row The row to the beginning of which the iterator has to point.
* @return An iterator that points to the beginning of the given row. * @return An iterator that points to the beginning of the given row.
*/ */
const_iterator begin(uint_fast64_t row = 0) const; const_iterator begin(IndexType row = 0) const;
/*! /*!
* Retrieves an iterator that points to the beginning of the given row. * Retrieves an iterator that points to the beginning of the given row.
@ -706,7 +723,7 @@ namespace storm {
* @param row The row to the beginning of which the iterator has to point. * @param row The row to the beginning of which the iterator has to point.
* @return An iterator that points to the beginning of the given row. * @return An iterator that points to the beginning of the given row.
*/ */
iterator begin(uint_fast64_t row = 0); iterator begin(IndexType row = 0);
/*! /*!
* Retrieves an iterator that points past the end of the given row. * Retrieves an iterator that points past the end of the given row.
@ -714,7 +731,7 @@ namespace storm {
* @param row The row past the end of which the iterator has to point. * @param row The row past the end of which the iterator has to point.
* @return An iterator that points past the end of the given row. * @return An iterator that points past the end of the given row.
*/ */
const_iterator end(uint_fast64_t row) const; const_iterator end(IndexType row) const;
/*! /*!
* Retrieves an iterator that points past the end of the given row. * Retrieves an iterator that points past the end of the given row.
@ -722,7 +739,7 @@ namespace storm {
* @param row The row past the end of which the iterator has to point. * @param row The row past the end of which the iterator has to point.
* @return An iterator that points past the end of the given row. * @return An iterator that points past the end of the given row.
*/ */
iterator end(uint_fast64_t row); iterator end(IndexType row);
/*! /*!
* Retrieves an iterator that points past the end of the last row of the matrix. * Retrieves an iterator that points past the end of the last row of the matrix.
@ -751,31 +768,31 @@ namespace storm {
* @return A matrix corresponding to a submatrix of the current matrix in which only row groups and columns * @return A matrix corresponding to a submatrix of the current matrix in which only row groups and columns
* given by the row group constraint are kept and all others are dropped. * given by the row group constraint are kept and all others are dropped.
*/ */
SparseMatrix getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector<uint_fast64_t> const& rowGroupIndices, bool insertDiagonalEntries = false) const; SparseMatrix getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector<IndexType> const& rowGroupIndices, bool insertDiagonalEntries = false) const;
// The number of rows of the matrix. // The number of rows of the matrix.
uint_fast64_t rowCount; IndexType rowCount;
// The number of columns of the matrix. // The number of columns of the matrix.
uint_fast64_t columnCount; IndexType columnCount;
// The number of entries in the matrix. // The number of entries in the matrix.
uint_fast64_t entryCount; IndexType entryCount;
// The number of nonzero entries in the matrix. // The number of nonzero entries in the matrix.
uint_fast64_t nonzeroEntryCount; IndexType nonzeroEntryCount;
// The storage for the columns and values of all entries in the matrix. // The storage for the columns and values of all entries in the matrix.
std::vector<MatrixEntry<T>> columnsAndValues; std::vector<MatrixEntry<IndexType, ValueType>> columnsAndValues;
// A vector containing the indices at which each given row begins. This index is to be interpreted as an // A vector containing the indices at which each given row begins. This index is to be interpreted as an
// index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries
// in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last
// entry is not included anymore. // entry is not included anymore.
std::vector<uint_fast64_t> rowIndications; std::vector<IndexType> rowIndications;
// A vector indicating the row groups of the matrix. // A vector indicating the row groups of the matrix.
std::vector<uint_fast64_t> rowGroupIndices; std::vector<IndexType> rowGroupIndices;
}; };
} // namespace storage } // namespace storage

8
src/storage/dd/CuddDd.cpp
View File

@ -496,7 +496,7 @@ namespace storm {
// Prepare the vectors that represent the matrix. // Prepare the vectors that represent the matrix.
std::vector<uint_fast64_t> rowIndications(rowOdd.getTotalOffset() + 1); std::vector<uint_fast64_t> rowIndications(rowOdd.getTotalOffset() + 1);
std::vector<storm::storage::MatrixEntry<double>> columnsAndValues(this->getNonZeroCount()); std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
// Create a trivial row grouping. // Create a trivial row grouping.
std::vector<uint_fast64_t> trivialRowGroupIndices(rowIndications.size()); std::vector<uint_fast64_t> trivialRowGroupIndices(rowIndications.size());
@ -584,7 +584,7 @@ namespace storm {
splitGroupsRec(this->getCuddAdd().getNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables); splitGroupsRec(this->getCuddAdd().getNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables);
// Create the actual storage for the non-zero entries. // Create the actual storage for the non-zero entries.
std::vector<storm::storage::MatrixEntry<double>> columnsAndValues(this->getNonZeroCount()); std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
// Now compute the indices at which the individual rows start. // Now compute the indices at which the individual rows start.
std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1); std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1);
@ -638,7 +638,7 @@ namespace storm {
return storm::storage::SparseMatrix<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); return storm::storage::SparseMatrix<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
} }
void Dd<DdType::CUDD>::toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues) const { void Dd<DdType::CUDD>::toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues) const {
// For the empty DD, we do not need to add any entries. // For the empty DD, we do not need to add any entries.
if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) { if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
return; return;
@ -647,7 +647,7 @@ namespace storm {
// If we are at the maximal level, the value to be set is stored as a constant in the DD. // If we are at the maximal level, the value to be set is stored as a constant in the DD.
if (currentRowLevel + currentColumnLevel == maxLevel) { if (currentRowLevel + currentColumnLevel == maxLevel) {
if (generateValues) { if (generateValues) {
columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry<double>(currentColumnOffset, Cudd_V(dd)); columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry<uint_fast64_t, double>(currentColumnOffset, Cudd_V(dd));
} }
++rowIndications[rowGroupOffsets[currentRowOffset]]; ++rowIndications[rowGroupOffsets[currentRowOffset]];
} else { } else {

2
src/storage/dd/CuddDd.h
View File

@ -685,7 +685,7 @@ namespace storm {
* only works if the offsets given in rowIndications are already correct. If they need to be computed first, * only works if the offsets given in rowIndications are already correct. If they need to be computed first,
* this flag needs to be false. * this flag needs to be false.
*/ */
void toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues = true) const; void toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues = true) const;
/*! /*!
* Splits the given matrix DD into the groups using the given group variables. * Splits the given matrix DD into the groups using the given group variables.

2
test/functional/storage/SparseMatrixTest.cpp
View File

@ -147,7 +147,7 @@ TEST(SparseMatrix, Build) {
} }
TEST(SparseMatrix, CreationWithMovingContents) { TEST(SparseMatrix, CreationWithMovingContents) {
std::vector<storm::storage::MatrixEntry<double>> columnsAndValues; std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues;
columnsAndValues.emplace_back(1, 1.0); columnsAndValues.emplace_back(1, 1.0);
columnsAndValues.emplace_back(2, 1.2); columnsAndValues.emplace_back(2, 1.2);
columnsAndValues.emplace_back(0, 0.5); columnsAndValues.emplace_back(0, 0.5);

Write Preview
|||||||
100:0
Loading…
Cancel
Save