diff --git a/resources/3rdparty/gmm-4.2/include/gmm/gmm_matrix.h b/resources/3rdparty/gmm-4.2/include/gmm/gmm_matrix.h index c7801bc15..2504786d5 100644 --- a/resources/3rdparty/gmm-4.2/include/gmm/gmm_matrix.h +++ b/resources/3rdparty/gmm-4.2/include/gmm/gmm_matrix.h @@ -491,7 +491,7 @@ namespace gmm template struct csc_matrix { - typedef unsigned int IND_TYPE; + typedef unsigned long long IND_TYPE; std::vector pr; std::vector ir; @@ -639,7 +639,7 @@ namespace gmm template struct csr_matrix { - typedef unsigned int IND_TYPE; + typedef unsigned long long IND_TYPE; std::vector pr; // values. std::vector ir; // col indices. diff --git a/src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h index 60c473b49..fbbaed0ea 100644 --- a/src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h @@ -10,7 +10,7 @@ #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/adapters/GmmxxAdapter.h" -#include "src/storage/JacobiDecomposition.h" +#include "src/storage/SparseMatrix.h" #include "src/utility/ConstTemplates.h" #include "src/utility/Settings.h" @@ -241,12 +241,12 @@ private: bool relative = s->get("relative"); // Get a Jacobi decomposition of the matrix A. - storm::storage::JacobiDecomposition* jacobiDecomposition = A.getJacobiDecomposition(); + storm::storage::SparseMatrix::SparseJacobiDecomposition_t jacobiDecomposition = A.getJacobiDecomposition(); // Convert the (inverted) diagonal matrix to gmm++'s format. - gmm::csr_matrix* gmmxxDiagonalInverted = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(jacobiDecomposition->getJacobiDInvReference()); + gmm::csr_matrix* gmmxxDiagonalInverted = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(std::move(jacobiDecomposition.second)); // Convert the LU matrix to gmm++'s format. - gmm::csr_matrix* gmmxxLU = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(jacobiDecomposition->getJacobiLUReference()); + gmm::csr_matrix* gmmxxLU = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(std::move(jacobiDecomposition.first)); LOG4CPLUS_INFO(logger, "Starting iterative Jacobi Solver."); @@ -295,7 +295,6 @@ private: // Also delete the other dynamically allocated variables. delete residuum; - delete jacobiDecomposition; delete gmmxxDiagonalInverted; delete gmmxxLU; diff --git a/src/storage/JacobiDecomposition.h b/src/storage/JacobiDecomposition.h deleted file mode 100644 index ef4f8bb99..000000000 --- a/src/storage/JacobiDecomposition.h +++ /dev/null @@ -1,105 +0,0 @@ -#ifndef STORM_STORAGE_JACOBIDECOMPOSITION_H_ -#define STORM_STORAGE_JACOBIDECOMPOSITION_H_ - -#include "boost/integer/integer_mask.hpp" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -#include "src/exceptions/InvalidAccessException.h" - -extern log4cplus::Logger logger; - -namespace storm { - -namespace storage { - -/*! - * Forward declaration against Cycle - */ -template -class SparseMatrix; - - -/*! - * A simple container for a sparse Jacobi decomposition - */ -template -class JacobiDecomposition { - -public: - /*! - * Standard constructor - * Initializes this object with the two given sparse matrices - * Ownership of both matrices stay with THIS object. - */ - JacobiDecomposition(storm::storage::SparseMatrix * const jacobiLuMatrix, storm::storage::SparseMatrix * const jacobiDInvMatrix) : jacobiLuMatrix(jacobiLuMatrix), jacobiDInvMatrix(jacobiDInvMatrix) { - } - - ~JacobiDecomposition() { - delete this->jacobiDInvMatrix; - delete this->jacobiLuMatrix; - } - - /*! - * Accessor for the internal LU Matrix. - * Ownership stays with this class. - * @return A reference to the Jacobi LU Matrix - */ - storm::storage::SparseMatrix& getJacobiLUReference() { - return *(this->jacobiLuMatrix); - } - - /*! - * Accessor for the internal D^{-1} Matrix. - * Ownership stays with this class. - * @return A reference to the Jacobi D^{-1} Matrix - */ - storm::storage::SparseMatrix& getJacobiDInvReference() { - return *(this->jacobiDInvMatrix); - } - - /*! - * Accessor for the internal LU Matrix. - * Ownership stays with this class. - * @return A pointer to the Jacobi LU Matrix - */ - storm::storage::SparseMatrix* getJacobiLU() { - return this->jacobiLuMatrix; - } - - /*! - * Accessor for the internal D^{-1} Matrix. - * Ownership stays with this class. - * @return A pointer to the Jacobi D^{-1} Matrix - */ - storm::storage::SparseMatrix* getJacobiDInv() { - return this->jacobiDInvMatrix; - } - -private: - - /*! - * The copy constructor is disabled for this class. - */ - //JacobiDecomposition(const JacobiDecomposition& that) = delete; // not possible in VS2012 - JacobiDecomposition(const JacobiDecomposition& that) { - throw storm::exceptions::InvalidAccessException() << "The copy constructor of JacobiDecomposition is explicitly disabled."; - } - - /*! - * Pointer to the LU Matrix - */ - storm::storage::SparseMatrix *jacobiLuMatrix; - - /*! - * Pointer to the D^{-1} Matrix - */ - storm::storage::SparseMatrix *jacobiDInvMatrix; -}; - -} // namespace storage - -} // namespace storm - -#endif // STORM_STORAGE_JACOBIDECOMPOSITION_H_ diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 12a0a6e93..8c880806c 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -14,7 +14,6 @@ #include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/FileIoException.h" #include "src/storage/BitVector.h" -#include "src/storage/JacobiDecomposition.h" #include "src/utility/ConstTemplates.h" #include "src/utility/Hash.h" @@ -46,6 +45,11 @@ namespace storage { template class SparseMatrix { public: + /*! + * Return Type of the Jacobi Decompostion + */ + typedef std::pair, storm::storage::SparseMatrix> SparseJacobiDecomposition_t; + /*! * Declare adapter classes as friends to use internal data. */ @@ -938,29 +942,30 @@ public: /*! * Calculates the Jacobi-Decomposition of this sparse matrix. * The source Sparse Matrix must be square. - * @return A pointer to a class containing the matrix L+U and the inverted diagonal matrix D^-1 + * @return A std::pair containing the matrix L+U and the inverted diagonal matrix D^-1 */ - storm::storage::JacobiDecomposition* getJacobiDecomposition() const { + SparseJacobiDecomposition_t getJacobiDecomposition() const { uint_fast64_t rowCount = this->getRowCount(); uint_fast64_t colCount = this->getColumnCount(); if (rowCount != colCount) { throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::getJacobiDecomposition requires the Matrix to be square."; } - storm::storage::SparseMatrix *resultLU = new storm::storage::SparseMatrix(*this); - storm::storage::SparseMatrix *resultDinv = new storm::storage::SparseMatrix(rowCount, colCount); + storm::storage::SparseMatrix resultLU(*this); + storm::storage::SparseMatrix resultDinv(rowCount, colCount); // no entries apart from those on the diagonal (rowCount) - resultDinv->initialize(rowCount); + resultDinv.initialize(rowCount); // constant 1 for diagonal inversion T constOne = storm::utility::constGetOne(); // copy diagonal entries to other matrix - for (unsigned int i = 0; i < rowCount; ++i) { - resultDinv->addNextValue(i, i, constOne / resultLU->getValue(i, i)); - resultLU->getValue(i, i) = storm::utility::constGetZero(); + for (uint_fast64_t i = 0; i < rowCount; ++i) { + resultDinv.addNextValue(i, i, constOne / resultLU.getValue(i, i)); + resultLU.getValue(i, i) = storm::utility::constGetZero(); } + resultDinv.finalize(); - return new storm::storage::JacobiDecomposition(resultLU, resultDinv); + return std::make_pair(std::move(resultLU), std::move(resultDinv)); } /*!