diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h new file mode 100644 index 000000000..ed3f2a893 --- /dev/null +++ b/src/adapters/GmmxxAdapter.h @@ -0,0 +1,108 @@ +/* + * GmmxxAdapter.h + * + * Created on: 24.12.2012 + * Author: Christian Dehnert + */ + +#ifndef GMMXXADAPTER_H_ +#define GMMXXADAPTER_H_ + +#include "src/storage/SquareSparseMatrix.h" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +namespace mrmc { + +namespace adapters { + +class GmmxxAdapter { +public: + /*! + * Converts a sparse matrix into the sparse matrix in the gmm++ format. + * @return A pointer to a column-major sparse matrix in gmm++ format. + */ + template + static gmm::csr_matrix* toGmmxxSparseMatrix(mrmc::storage::SquareSparseMatrix const& matrix) { + uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount() + matrix.getDiagonalNonZeroEntryCount(); + LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); + + // Prepare the resulting matrix. + gmm::csr_matrix* result = new gmm::csr_matrix(matrix.rowCount, matrix.rowCount); + + // Reserve enough elements for the row indications. + result->jc.reserve(matrix.rowCount + 1); + + // For the column indications and the actual values, we have to gather + // the values in a temporary array first, as we have to integrate + // the values from the diagonal. For the row indications, we can just count the number of + // inserted diagonal elements and add it to the previous value. + uint_fast64_t* tmpColumnIndicationsArray = new uint_fast64_t[realNonZeros]; + T* tmpValueArray = new T[realNonZeros]; + T zero(0); + uint_fast64_t currentPosition = 0; + uint_fast64_t insertedDiagonalElements = 0; + for (uint_fast64_t i = 0; i < matrix.rowCount; ++i) { + // Compute correct start index of row. + result->jc[i] = matrix.rowIndications[i] + insertedDiagonalElements; + + // If the current row has no non-zero which is not on the diagonal, we have to check the + // diagonal element explicitly. + if (matrix.rowIndications[i + 1] - matrix.rowIndications[i] == 0) { + if (matrix.diagonalStorage[i] != zero) { + tmpColumnIndicationsArray[currentPosition] = i; + tmpValueArray[currentPosition] = matrix.diagonalStorage[i]; + ++currentPosition; ++insertedDiagonalElements; + } + } else { + // Otherwise, we can just enumerate the non-zeros which are not on the diagonal + // and fit in the diagonal element where appropriate. + bool includedDiagonal = false; + for (uint_fast64_t j = matrix.rowIndications[i]; j < matrix.rowIndications[i + 1]; ++j) { + if (matrix.diagonalStorage[i] != zero && !includedDiagonal && matrix.columnIndications[j] > i) { + includedDiagonal = true; + tmpColumnIndicationsArray[currentPosition] = i; + tmpValueArray[currentPosition] = matrix.diagonalStorage[i]; + ++currentPosition; ++insertedDiagonalElements; + } + tmpColumnIndicationsArray[currentPosition] = matrix.columnIndications[j]; + tmpValueArray[currentPosition] = matrix.valueStorage[j]; + ++currentPosition; + } + + // If the diagonal element is non-zero and was not inserted until now (i.e. all + // off-diagonal elements in the row are before the diagonal element. + if (!includedDiagonal && matrix.diagonalStorage[i] != zero) { + tmpColumnIndicationsArray[currentPosition] = i; + tmpValueArray[currentPosition] = matrix.diagonalStorage[i]; + ++currentPosition; ++insertedDiagonalElements; + } + } + } + // Fill in sentinel element at the end. + result->jc[matrix.rowCount] = static_cast(realNonZeros); + + // Now, we can copy the temporary array to the GMMXX format. + result->ir.resize(realNonZeros); + std::copy(tmpColumnIndicationsArray, tmpColumnIndicationsArray + realNonZeros, result->ir.begin()); + delete[] tmpColumnIndicationsArray; + + // And do the same thing with the actual values. + result->pr.resize(realNonZeros); + std::copy(tmpValueArray, tmpValueArray + realNonZeros, result->pr.begin()); + delete[] tmpValueArray; + + LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format."); + + return result; + } +}; + +} //namespace adapters + +} //namespace mrmc + +#endif /* GMMXXADAPTER_H_ */ diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 454af57f2..bc4582519 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -16,6 +16,7 @@ #include "src/utility/Vector.h" #include "src/utility/ConstTemplates.h" #include "src/utility/Settings.h" +#include "src/adapters/GmmxxAdapter.h" #include "gmm/gmm_matrix.h" #include "gmm/gmm_iter_solvers.h" @@ -52,7 +53,7 @@ public: tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix(); + gmm::csr_matrix* gmmxxMatrix = mrmc::adapters::GmmxxAdapter::toGmmxxSparseMatrix(tmpMatrix); // Create the vector with which to multiply. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); @@ -80,7 +81,7 @@ public: mrmc::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = this->getModel().getTransitionProbabilityMatrix()->toGMMXXSparseMatrix(); + gmm::csr_matrix* gmmxxMatrix = mrmc::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionProbabilityMatrix()); // Create the vector with which to multiply and initialize it correctly. std::vector x(this->getModel().getNumberOfStates()); @@ -133,7 +134,7 @@ public: submatrix->convertToEquationSystem(); // Transform the submatrix to the gmm++ format to use its solvers. - gmm::csr_matrix* gmmxxMatrix = submatrix->toGMMXXSparseMatrix(); + gmm::csr_matrix* gmmxxMatrix = mrmc::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*submatrix); delete submatrix; // Initialize the x vector with 0.5 for each element. This is the initial guess for diff --git a/src/parser/AutoTransitionParser.cpp b/src/parser/AutoTransitionParser.cpp index 93e5fc383..402e8e14e 100644 --- a/src/parser/AutoTransitionParser.cpp +++ b/src/parser/AutoTransitionParser.cpp @@ -76,4 +76,5 @@ std::pair AutoTransitionParser::analyzeContent(co } } //namespace parser -} //namespace mrmc \ No newline at end of file + +} //namespace mrmc diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index d95009bf1..2132ba42c 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -23,6 +23,9 @@ extern log4cplus::Logger logger; +// Forward declaration for adapter classes. +namespace mrmc { namespace adapters{ class GmmxxAdapter; } } + namespace mrmc { namespace storage { @@ -36,6 +39,10 @@ namespace storage { template class SquareSparseMatrix { public: + /*! + * Declare adapter classes as friends to use internal data. + */ + friend class mrmc::adapters::GmmxxAdapter; /*! * If we only want to iterate over the columns of the non-zero entries of @@ -613,84 +620,6 @@ public: return nullptr; } - /*! - * Converts the matrix into a sparse matrix in the GMMXX format. - * @return A pointer to a column-major sparse matrix in GMMXX format. - */ - gmm::csr_matrix* toGMMXXSparseMatrix() { - uint_fast64_t realNonZeros = getNonZeroEntryCount() + getDiagonalNonZeroEntryCount(); - LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); - - // Prepare the resulting matrix. - gmm::csr_matrix* result = new gmm::csr_matrix(rowCount, rowCount); - - // Reserve enough elements for the row indications. - result->jc.reserve(rowCount + 1); - - // For the column indications and the actual values, we have to gather - // the values in a temporary array first, as we have to integrate - // the values from the diagonal. For the row indications, we can just count the number of - // inserted diagonal elements and add it to the previous value. - uint_fast64_t* tmpColumnIndicationsArray = new uint_fast64_t[realNonZeros]; - T* tmpValueArray = new T[realNonZeros]; - T zero(0); - uint_fast64_t currentPosition = 0; - uint_fast64_t insertedDiagonalElements = 0; - for (uint_fast64_t i = 0; i < rowCount; ++i) { - // Compute correct start index of row. - result->jc[i] = rowIndications[i] + insertedDiagonalElements; - - // If the current row has no non-zero which is not on the diagonal, we have to check the - // diagonal element explicitly. - if (rowIndications[i + 1] - rowIndications[i] == 0) { - if (diagonalStorage[i] != zero) { - tmpColumnIndicationsArray[currentPosition] = i; - tmpValueArray[currentPosition] = diagonalStorage[i]; - ++currentPosition; ++insertedDiagonalElements; - } - } else { - // Otherwise, we can just enumerate the non-zeros which are not on the diagonal - // and fit in the diagonal element where appropriate. - bool includedDiagonal = false; - for (uint_fast64_t j = rowIndications[i]; j < rowIndications[i + 1]; ++j) { - if (diagonalStorage[i] != zero && !includedDiagonal && columnIndications[j] > i) { - includedDiagonal = true; - tmpColumnIndicationsArray[currentPosition] = i; - tmpValueArray[currentPosition] = diagonalStorage[i]; - ++currentPosition; ++insertedDiagonalElements; - } - tmpColumnIndicationsArray[currentPosition] = columnIndications[j]; - tmpValueArray[currentPosition] = valueStorage[j]; - ++currentPosition; - } - - // If the diagonal element is non-zero and was not inserted until now (i.e. all - // off-diagonal elements in the row are before the diagonal element. - if (!includedDiagonal && diagonalStorage[i] != zero) { - tmpColumnIndicationsArray[currentPosition] = i; - tmpValueArray[currentPosition] = diagonalStorage[i]; - ++currentPosition; ++insertedDiagonalElements; - } - } - } - // Fill in sentinel element at the end. - result->jc[rowCount] = static_cast(realNonZeros); - - // Now, we can copy the temporary array to the GMMXX format. - result->ir.resize(realNonZeros); - std::copy(tmpColumnIndicationsArray, tmpColumnIndicationsArray + realNonZeros, result->ir.begin()); - delete[] tmpColumnIndicationsArray; - - // And do the same thing with the actual values. - result->pr.resize(realNonZeros); - std::copy(tmpValueArray, tmpValueArray + realNonZeros, result->pr.begin()); - delete[] tmpValueArray; - - LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format."); - - return result; - } - /*! * Returns the number of non-zero entries that are not on the diagonal. * @returns The number of non-zero entries that are not on the diagonal.