From 4bb76d026895426fd42f8a712fb89d79b89fdb33 Mon Sep 17 00:00:00 2001 From: PBerger Date: Thu, 24 Jan 2013 01:18:22 +0100 Subject: [PATCH] Added EigenAdapter and a Test for the Adapter. Fixed a type in EigenDtmcPrctlModelChecker.h Added missing transitions in one example input file --- src/adapters/EigenAdapter.h | 57 +++++++++++ src/modelChecker/EigenDtmcPrctlModelChecker.h | 2 +- src/storage/SparseMatrix.h | 3 +- test/eigen/EigenAdapterTest.cpp | 96 +++++++++++++++++++ 4 files changed, 156 insertions(+), 2 deletions(-) create mode 100644 src/adapters/EigenAdapter.h create mode 100644 test/eigen/EigenAdapterTest.cpp diff --git a/src/adapters/EigenAdapter.h b/src/adapters/EigenAdapter.h new file mode 100644 index 000000000..d7c8169e0 --- /dev/null +++ b/src/adapters/EigenAdapter.h @@ -0,0 +1,57 @@ +/* + * EigenAdapter.h + * + * Created on: 21.01.2013 + * Author: Philipp Berger + */ + +#ifndef STORM_ADAPTERS_EIGENADAPTER_H_ +#define STORM_ADAPTERS_EIGENADAPTER_H_ + +#include "src/storage/SparseMatrix.h" +#include "Eigen/Sparse" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +namespace storm { + +namespace adapters { + +class EigenAdapter { +public: + /*! + * Converts a sparse matrix into the sparse matrix in the eigen format. + * @return A pointer to a row-major sparse matrix in eigen format. + */ + template + static Eigen::SparseMatrix* toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix) { + uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount(); + LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to Eigen format."); + + // Prepare the resulting matrix. + Eigen::SparseMatrix* result = new Eigen::SparseMatrix(matrix.rowCount, matrix.colCount); + + result->resizeNonZeros(realNonZeros); + //result->reserve(realNonZeros); + + // Copy Row Indications + std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), (result->outerIndexPtr())); + // Copy Columns Indications + std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), (result->innerIndexPtr())); + // And do the same thing with the actual values. + std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), (result->valuePtr())); + + LOG4CPLUS_DEBUG(logger, "Done converting matrix to Eigen format."); + + return result; + } +}; + +} //namespace adapters + +} //namespace storm + +#endif /* STORM_ADAPTERS_GMMXXADAPTER_H_ */ diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h index e6ea58725..26a18cd8d 100644 --- a/src/modelChecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h @@ -87,7 +87,7 @@ public: // First, we need to compute the states that satisfy the sub-formula of the next-formula. storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. + // Transform the transition probability matrix to the eigen format to use its arithmetic. Eigen::SparseMatrix* eigenMatrix = this->getModel().getTransitionProbabilityMatrix()->toEigenSparseMatrix(); // Create the vector with which to multiply and initialize it correctly. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 481ddb93e..fb06f905f 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -25,7 +25,7 @@ extern log4cplus::Logger logger; // Forward declaration for adapter classes. -namespace storm { namespace adapters{ class GmmxxAdapter; } } +namespace storm { namespace adapters{ class GmmxxAdapter; class EigenAdapter; } } namespace storm { @@ -43,6 +43,7 @@ public: * Declare adapter classes as friends to use internal data. */ friend class storm::adapters::GmmxxAdapter; + friend class storm::adapters::EigenAdapter; /*! * If we only want to iterate over the columns of the non-zero entries of diff --git a/test/eigen/EigenAdapterTest.cpp b/test/eigen/EigenAdapterTest.cpp new file mode 100644 index 000000000..bddb74dd7 --- /dev/null +++ b/test/eigen/EigenAdapterTest.cpp @@ -0,0 +1,96 @@ +#include "gtest/gtest.h" + +#include "Eigen/Sparse" +#include "src/adapters/EigenAdapter.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "boost/integer/integer_mask.hpp" + +#define STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5 +#define STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5 + +TEST(EigenAdapterTest, SimpleDenseSquareCopy) { + // 5 rows + storm::storage::SparseMatrix sm(STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); + + double values[STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE]; + sm.initialize(STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); + + int row = 0; + int col = 0; + for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { + values[i] = static_cast(i + 1); + + sm.addNextValue(row, col, values[i]); + ++col; + if (col == STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { + ++row; + col = 0; + } + } + sm.finalize(); + + auto esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(sm); + + ASSERT_EQ(esm->rows(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); + ASSERT_EQ(esm->cols(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); + ASSERT_EQ(esm->nonZeros(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); + + row = 0; + col = 0; + for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { + ASSERT_EQ(values[i], esm->coeff(row, col)); + ++col; + if (col == STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { + ++row; + col = 0; + } + } +} + +TEST(EigenAdapterTest, SimpleSparseSquareCopy) { + // 5 rows + storm::storage::SparseMatrix sm(STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); + + double values[STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE]; + sm.initialize((STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); + + int row = 0; + int col = 0; + + bool everySecondElement = true; + + for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { + values[i] = static_cast(i + 1); + if (everySecondElement) { + sm.addNextValue(row, col, values[i]); + } + everySecondElement = !everySecondElement; + ++col; + if (col == STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { + ++row; + col = 0; + } + } + sm.finalize(); + + auto esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(sm); + + ASSERT_EQ(esm->rows(), STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); + ASSERT_EQ(esm->cols(), STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); + ASSERT_EQ(esm->nonZeros(), (STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); + + row = 0; + col = 0; + everySecondElement = true; + for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { + if (everySecondElement) { + ASSERT_EQ(values[i], esm->coeff(row, col)); + } + everySecondElement = !everySecondElement; + ++col; + if (col == STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { + ++row; + col = 0; + } + } +}