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

@@ -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<class T>
+	static Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>* toEigenSparseMatrix(storm::storage::SparseMatrix<T> 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<T, Eigen::RowMajor, int_fast32_t>* result = new Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>(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_ */

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<Type, 1, int_fast32_t>* eigenMatrix = this->getModel().getTransitionProbabilityMatrix()->toEigenSparseMatrix();
 
 		// Create the vector with which to multiply and initialize it correctly.

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

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<double> 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<double>(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<double> 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<double>(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;
+		}
+	}
+}