Added more example files. Removed deletes at end of main() as these pointers are deleted by the DTMC class already. Small refactoring of GraphAnalyzer according to new guidelines. Added vector utility functions to set elements of vectors. Added conversion routine from our sparse matrix format to gmm++ format. Fixed some bugs in sparse matrix class. Added prototypical implementation of GmmxxDtmcPrctlModelChecker.

src/modelChecker/DtmcPrctlModelChecker.h

@@ -166,7 +166,7 @@ public:
 	 * @param formula The Or state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or<T>& formula) {
+	virtual mrmc::storage::BitVector* checkOr(mrmc::formula::Or<T>& formula) {
 		mrmc::storage::BitVector* result = check(formula.getLeft());
 		mrmc::storage::BitVector* right = check(formula.getRight());
 		(*result) |= (*right);

src/modelChecker/GmmxxDtmcPrctlModelChecker.h

@@ -0,0 +1,162 @@
+/*
+ * GmmxxDtmcPrctlModelChecker.h
+ *
+ *  Created on: 06.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef GMMXXDTMCPRCTLMODELCHECKER_H_
+#define GMMXXDTMCPRCTLMODELCHECKER_H_
+
+#include "src/utility/vector.h"
+
+#include "src/models/dtmc.h"
+#include "src/solver/GraphAnalyzer.h"
+
+#include "gmm/gmm_matrix.h"
+#include "gmm/gmm_iter_solvers.h"
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+log4cplus::Logger logger;
+
+namespace mrmc {
+
+namespace modelChecker {
+
+/*
+ * A model checking engine that makes use of the gmm++ backend.
+ */
+template <class T>
+class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker<T> {
+
+public:
+	explicit GmmxxDtmcPrctlModelChecker(const mrmc::models::Dtmc<T>* dtmc) : DtmcPrctlModelChecker(dtmc) { }
+
+	virtual ~GmmxxDtmcPrctlModelChecker() { }
+
+	virtual std::vector<T>* checkBoundedUntil(mrmc::formula::BoundedUntil<T>& formula) {
+		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
+		mrmc::storage::BitVector* leftStates = this->check(formula.getLeft());
+		mrmc::storage::BitVector* rightStates = this->check(formula.getRight());
+
+		// Copy the matrix before we make any changes.
+		mrmc::storage::SquareSparseMatrix<T>* tmpMatrix(dtmc.getTransitionProbabilityMatrix());
+
+		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
+		tmpMatrix.makeRowsAbsorbing((~leftStates & rightStates) | rightStates);
+
+		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
+		gmm::csr_matrix<double>* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix();
+
+		// Create the vector with which to multiply.
+		std::vector<T>* result = new st::vector<T>(dtmc.getNumberOfStates());
+		mrmc::utility::setVectorValue(result, *rightStates, 1);
+
+		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
+		for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
+			gmm::mult(*gmmxxMatrix, *result, *result);
+		}
+
+		// Delete intermediate results.
+		delete leftStates;
+		delete rightStates;
+
+		return result;
+	}
+
+	virtual std::vector<T>* checkNext(const mrmc::formula::Next<T>& formula) {
+		// First, we need to compute the states that satisfy the sub-formula of the next-formula.
+		mrmc::storage::BitVector* nextStates = this->check(formula.getChild());
+
+		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
+		gmm::csr_matrix<double>* gmmxxMatrix = dtmc.getTransitionProbabilityMatrix()->toGMMXXSparseMatrix();
+
+		// Create the vector with which to multiply and initialize it correctly.
+		std::vector<T> x(dtmc.getNumberOfStates());
+		mrmc::utility::setVectorValue(x, nextStates, 1);
+
+		// Delete not needed next states bit vector.
+		delete nextStates;
+
+		// Create resulting vector.
+		std::vector<T>* result = new std::vector<T>(dtmc.getNumberOfStates());
+
+		// Perform the actual computation.
+		gmm::mult(*gmmxxMatrix, x, *result);
+
+		// Delete temporary matrix and return result.
+		delete gmmxxMatrix;
+		return result;
+	}
+
+	virtual std::vector<T>* checkUntil(const mrmc::formula::Until<T>& formula) {
+		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
+		mrmc::storage::BitVector* leftStates = this->check(formula.getLeft());
+		mrmc::storage::BitVector* rightStates = this->check(formula.getRight());
+
+		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
+		// all states that have probability 0 and 1 of satisfying the until-formula.
+		mrmc::storage::BitVector notExistsPhiUntilPsiStates(dtmc.getNumberOfStates());
+		mrmc::storage::BitVector alwaysPhiUntilPsiStates(dtmc.getNumberOfStates());
+		mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates<double>(dtmc, *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
+		notExistsPhiUntilPsiStates->complement();
+
+		delete leftStates;
+		delete rightStates;
+
+		LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states.");
+		LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states.");
+		mrmc::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates);
+		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " maybe states.");
+
+		// Only try to solve system if there are states for which the probability is unknown.
+		if (maybeStates.getNumberOfSetBits() > 0) {
+			// Now we can eliminate the rows and columns from the original transition probability matrix.
+			mrmc::storage::SquareSparseMatrix<double>* submatrix = dtmc.getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
+			// Converting the matrix to the form needed for the equation system. That is, we go from
+			// x = A*x + b to (I-A)x = b.
+			submatrix->convertToEquationSystem();
+
+			// Transform the submatrix to the gmm++ format to use its solvers.
+			gmm::csr_matrix<double>* gmmxxMatrix = submatrix->toGMMXXSparseMatrix();
+
+			// Initialize the x vector with 0.5 for each element. This is the initial guess for
+			// the iterative solvers. It should be safe as for all 'maybe' states we know that the
+			// probability is strictly larger than 0.
+			std::vector<T>* x = new std::vector<T>(maybeStates.getNumberOfSetBits(), 0.5);
+
+			// Prepare the right-hand side of the equation system. For entry i this corresponds to
+			// the accumulated probability of going from state i to some 'yes' state.
+			std::vector<double> b(maybeStates.getNumberOfSetBits());
+			dtmc.getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x);
+
+			// Set up the precondition of the iterative solver.
+			gmm::ilu_precond<gmm::csr_matrix<double>> P(*gmmxxMatrix);
+			// Prepare an iteration object that determines the accuracy, maximum number of iterations
+			// and the like.
+			gmm::iteration iter(0.000001);
+
+			// Now do the actual solving.
+			LOG4CPLUS_INFO(logger, "Starting iterations...");
+			gmm::bicgstab(*gmmxxMatrix, x, b, P, iter);
+			LOG4CPLUS_INFO(logger, "Done with iterations.");
+
+			// Create resulting vector and set values accordingly.
+			std::vector<T>* result = new std::vector<T>(dtmc.getNumberOfStates());
+			mrmc::utility::setVectorValues<std::vector<T>>(result, maybeStates, x);
+
+			// Delete temporary matrix and return result.
+			delete x;
+			delete gmmxxMatrix;
+		}
+
+		mrmc::utility::setVectorValue<std::vector<T>>(result, notExistsPhiUntilPsiStates, 0);
+		mrmc::utility::setVectorValue<std::vector<T>>(result, alwaysPhiUntilPsiStates, 1);
+
+		return result;
+	}
+};
+
+#endif /* GMMXXDTMCPRCTLMODELCHECKER_H_ */

src/mrmc.cpp

@@ -15,6 +15,7 @@
 #include <iostream>
 #include <cstdio>
 #include <sstream>
+#include <vector>
 
 #include "mrmc-config.h"
 #include "src/models/Dtmc.h"
@@ -25,8 +26,6 @@
 #include "src/parser/readPrctlFile.h"
 #include "src/solver/GraphAnalyzer.h"
 #include "src/utility/settings.h"
-#include "Eigen/Sparse"
-#include "gmm/gmm_matrix.h"
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
@@ -107,9 +106,6 @@ int main(const int argc, const char* argv[]) {
 		delete s;
 	}
 	
-	delete labparser.getLabeling();
-	delete traparser.getMatrix();
-
 	LOG4CPLUS_INFO(logger, "Nothing more to do, exiting.");
 
 	return 0;

src/solver/GraphAnalyzer.h

@@ -9,8 +9,12 @@
 #define GRAPHANALYZER_H_
 
 #include "src/models/Dtmc.h"
+#include "src/exceptions/invalid_argument.h"
 
-#include <iostream>
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+extern log4cplus::Logger logger;
 
 namespace mrmc {
 
@@ -24,17 +28,24 @@ public:
 	 * of the given target states whilst always staying in the set of filter states
 	 * before. The resulting states are written to the given bit vector.
 	 * @param model The model whose graph structure to search.
-	 * @param targetStates The target states of the search.
-	 * @param filterStates A set of states constraining the search.
-	 * @param existentialReachabilityStates The result of the search.
+	 * @param phiStates A bit vector of all states satisfying phi.
+	 * @param psiStates A bit vector of all states satisfying psi.
+	 * @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess
+	 * a paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void getExistsPhiUntilPsiStates(mrmc::models::Dtmc<T>& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector& existsPhiUntilPsiStates) {
+	static void getExistsPhiUntilPsiStates(mrmc::models::Dtmc<T>& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector* existsPhiUntilPsiStates) {
+		// Check for valid parameter.
+		if (existsPhiUntilPsiStates == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null.");
+			throw mrmc::exceptions::invalid_argument("Parameter 'existsPhiUntilPhiStates' must not be null.");
+		}
+
 		// Get the backwards transition relation from the model to ease the search.
 		mrmc::models::GraphTransitions<T>& backwardTransitions = model.getBackwardTransitions();
 
 		// Add all psi states as the already satisfy the condition.
-		existsPhiUntilPsiStates |= psiStates;
+		*existsPhiUntilPsiStates |= psiStates;
 
 		// Initialize the stack used for the DFS with the states
 		std::vector<uint_fast64_t> stack;
@@ -47,8 +58,8 @@ public:
 			stack.pop_back();
 
 			for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
-				if (phiStates.get(*it) && !existsPhiUntilPsiStates.get(*it)) {
-					existsPhiUntilPsiStates.set(*it, true);
+				if (phiStates.get(*it) && !existsPhiUntilPsiStates->get(*it)) {
+					existsPhiUntilPsiStates->set(*it, true);
 					stack.push_back(*it);
 				}
 			}
@@ -62,16 +73,23 @@ public:
 	 * characterizes the states that possess at least one path to a target state.
 	 * The results are written to the given bit vector.
 	 * @param model The model whose graph structure to search.
-	 * @param targetStates The target states of the search.
-	 * @param filterStates A set of states constraining the search.
-	 * @param existentialReachabilityStates The set of states that possess at
-	 * least one path to a target state.
-	 * @param universalReachabilityStates The result of the search.
+	 * @param phiStates A bit vector of all states satisfying phi.
+	 * @param psiStates A bit vector of all states satisfying psi.
+	 * @param existsPhiUntilPsiStates A reference to a bit vector of states that possess a path
+	 * satisfying phi until psi.
+	 * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
+	 * have paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void getAlwaysPhiUntilPsiStates(mrmc::models::Dtmc<T>& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, const mrmc::storage::BitVector& existsPhiUntilPsiStates, mrmc::storage::BitVector& alwaysPhiUntilPsiStates) {
+	static void getAlwaysPhiUntilPsiStates(mrmc::models::Dtmc<T>& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, const mrmc::storage::BitVector& existsPhiUntilPsiStates, mrmc::storage::BitVector* alwaysPhiUntilPsiStates) {
+		// Check for valid parameter.
+		if (alwaysPhiUntilPsiStates == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null.");
+			throw mrmc::exceptions::invalid_argument("Parameter 'alwaysPhiUntilPhiStates' must not be null.");
+		}
+
 		GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates);
-		alwaysPhiUntilPsiStates.complement();
+		alwaysPhiUntilPsiStates->complement();
 	}
 
 	/*!
@@ -79,15 +97,28 @@ public:
 	 * the given set of target states and only visit states from the filter set
 	 * before.
 	 * @param model The model whose graph structure to search.
-	 * @param targetStates The target states of the search.
-	 * @param filterStates A set of states constraining the search.
-	 * @param universalReachabilityStates The result of the search.
+	 * @param phiStates A bit vector of all states satisfying phi.
+	 * @param psiStates A bit vector of all states satisfying psi.
+	 * @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess
+	 * a path satisfying phi until psi.
+	 * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
+	 * have paths satisfying phi until psi.
 	 */
 	template <class T>
-	static void getAlwaysPhiUntilPsiStates(mrmc::models::Dtmc<T>& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector& alwaysPhiUntilPsiStates) {
-		mrmc::storage::BitVector existsPhiUntilPsiStates(model.getNumberOfStates());
+	static void getPhiUntilPsiStates(mrmc::models::Dtmc<T>& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector* existsPhiUntilPsiStates, mrmc::storage::BitVector* alwaysPhiUntilPsiStates) {
+		// Check for valid parameters.
+		if (existsPhiUntilPsiStates == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null.");
+			throw mrmc::exceptions::invalid_argument("Parameter 'existsPhiUntilPhiStates' must not be null.");
+		}
+		if (alwaysPhiUntilPsiStates == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null.");
+			throw mrmc::exceptions::invalid_argument("Parameter 'alwaysPhiUntilPhiStates' must not be null.");
+		}
+
+		// Perform search.
 		GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, existsPhiUntilPsiStates);
-		GraphAnalyzer::getAlwaysPhiUntilPsiStates(model, phiStates, psiStates, existsPhiUntilPsiStates, alwaysPhiUntilPsiStates);
+		GraphAnalyzer::getAlwaysPhiUntilPsiStates(model, phiStates, psiStates, *existsPhiUntilPsiStates, alwaysPhiUntilPsiStates);
 	}
 
 };

src/storage/SquareSparseMatrix.h

@@ -4,6 +4,7 @@
 #include <exception>
 #include <new>
 #include <algorithm>
+#include <iostream>
 #include "boost/integer/integer_mask.hpp"
 
 #include "src/exceptions/invalid_state.h"
@@ -113,19 +114,15 @@ public:
 	~SquareSparseMatrix() {
 		setState(MatrixStatus::UnInitialized);
 		if (valueStorage != nullptr) {
-			//free(value_storage);
 			delete[] valueStorage;
 		}
 		if (columnIndications != nullptr) {
-			//free(column_indications);
 			delete[] columnIndications;
 		}
 		if (rowIndications != nullptr) {
-			//free(row_indications);
 			delete[] rowIndications;
 		}
 		if (diagonalStorage != nullptr) {
-			//free(diagonal_storage);
 			delete[] diagonalStorage;
 		}
 	}
@@ -570,40 +567,66 @@ public:
 	 * @return A pointer to a column-major sparse matrix in GMMXX format.
 	 */
 	gmm::csr_matrix<T>* 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<T>* result = new gmm::csr_matrix<T>(rowCount, rowCount);
 
-		LOG4CPLUS_INFO(logger, "Starting copy1.");
-		// Copy over the row indications as GMMXX uses the very same internal format.
+		// Reserve enough elements for the row indications.
 		result->jc.reserve(rowCount + 1);
-		std::copy(rowIndications, rowIndications + (rowCount + 1), result->jc.begin());
-		LOG4CPLUS_INFO(logger, "Done copy1.");
 
 		// 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.
-		uint_fast64_t realNonZeros = getNonZeroEntryCount() + getDiagonalNonZeroEntryCount();
+		// 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];
-		uint_fast64_t* tmpValueArray = 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) {
-			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;
+			// 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;
 				}
-				tmpColumnIndicationsArray[currentPosition] = columnIndications[j];
-				tmpValueArray[currentPosition] = valueStorage[j];
+
+				// 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] = realNonZeros;
 
-		LOG4CPLUS_INFO(logger, "Starting copy2.");
 		// Now, we can copy the temporary array to the GMMXX format.
-		result->ir.reserve(realNonZeros);
+		result->ir.resize(realNonZeros);
 		std::copy(tmpColumnIndicationsArray, tmpColumnIndicationsArray + realNonZeros, result->ir.begin());
 		delete[] tmpColumnIndicationsArray;
 
@@ -611,7 +634,8 @@ public:
 		result->pr.resize(realNonZeros);
 		std::copy(tmpValueArray, tmpValueArray + realNonZeros, result->pr.begin());
 		delete[] tmpValueArray;
-		LOG4CPLUS_INFO(logger, "Done copy2.");
+
+		LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format.");
 
 		return result;
 	}
@@ -637,6 +661,15 @@ public:
 		return result;
 	}
 
+	/*!
+	 * This function makes the rows given by the bit vector absorbing.
+	 */
+	bool makeRowsAbsorbing(const mrmc::storage::BitVector rows) {
+		for (auto row : rows) {
+			makeRowAbsorbing(row);
+		}
+	}
+
 	/*!
 	 * This function makes the given row absorbing. This means that all
 	 * entries in will be set to 0 and the value 1 will be written
@@ -688,13 +721,15 @@ public:
 	/*!
 	 * Computes a vector in which each element is the sum of those elements in the
 	 * corresponding row whose column bits are set to one in the given constraint.
-	 * @param constraint A bit vector that indicates which columns to add.
+	 * @param rowConstraint A bit vector that indicates for which rows to perform summation.
+	 * @param columnConstraint A bit vector that indicates which columns to add.
 	 * @param resultVector A pointer to the resulting vector that has at least
 	 * as many elements as there are bits set to true in the constraint.
 	 */
-	void getConstrainedRowCountVector(const mrmc::storage::BitVector& constraint, T* resultVector) {
-		for (uint_fast64_t row = 0; row < rowCount; ++row) {
-			resultVector[row] = getConstrainedRowSum(row, constraint);
+	void getConstrainedRowCountVector(const mrmc::storage::BitVector& rowConstraint, const mrmc::storage::BitVector& columnConstraint, std::vector<T>* resultVector) {
+		uint_fast64_t currentRowCount = 0;
+		for (auto row : rowConstraint) {
+			resultVector[currentRowCount++] = getConstrainedRowSum(row, columnConstraint);
 		}
 	}
 
@@ -724,8 +759,6 @@ public:
 			}
 		}
 
-		LOG4CPLUS_DEBUG(logger, "Done counting non-zeros.");
-
 		// Create and initialize resulting matrix.
 		SquareSparseMatrix* result = new SquareSparseMatrix(constraint.getNumberOfSetBits());
 		result->initialize(subNonZeroEntries);
@@ -765,6 +798,31 @@ public:
 		return result;
 	}
 
+	void convertToEquationSystem() {
+		invertDiagonal();
+		negateAllNonDiagonalElements();
+	}
+
+	/*!
+	 * Inverts all elements on the diagonal, i.e. sets the diagonal values to 1 minus their previous
+	 * value.
+	 */
+	void invertDiagonal() {
+		T one(1);
+		for (uint_fast64_t i = 0; i < rowCount; ++i) {
+			diagonalStorage[i] = one - diagonalStorage[i];
+		}
+	}
+
+	/*!
+	 * Negates all non-zero elements that are not on the diagonal.
+	 */
+	void negateAllNonDiagonalElements() {
+		for (uint_fast64_t i = 0; i < nonZeroEntryCount; ++i) {
+			valueStorage[i] = - valueStorage[i];
+		}
+	}
+
 	/*!
 	 * Returns the size of the matrix in memory measured in bytes.
 	 * @return The size of the matrix in memory measured in bytes.
@@ -802,6 +860,19 @@ public:
 		return this->columnIndications + this->rowIndications[row + 1];
 	}
 
+	void print() {
+		std::cout << "diag: --------------------------------" << std::endl;
+		for (uint_fast64_t i = 0; i < rowCount; ++i) {
+			std::cout << "(" << i << "," << i << ") = " << diagonalStorage[i] << std::endl;
+		}
+		std::cout << "non diag: ----------------------------" << std::endl;
+		for (uint_fast64_t i = 0; i < rowCount; ++i) {
+			for (uint_fast64_t j = rowIndications[i]; j < rowIndications[i + 1]; ++j) {
+				std::cout << "(" << i << "," << columnIndications[j] << ") = " << valueStorage[j] << std::endl;
+			}
+		}
+	}
+
 private:
 
 	/*!

src/utility/vector.h

@@ -0,0 +1,34 @@
+/*
+ * vector.h
+ *
+ *  Created on: 06.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef VECTOR_H_
+#define VECTOR_H_
+
+namespace mrmc {
+
+namespace utility {
+
+template<T>
+void setVectorValues(std::vector<T>* vector, const mrmc::storage::BitVector& positions, std::vector<T>* values) {
+	uint_fast64_t oldPosition = 0;
+	for (auto position : positions) {
+		vector[position] = values[oldPosition++];
+	}
+}
+
+template<T>
+void setVectorValue(std::vector<T>* vector, const mrmc::storage::BitVector& positions, T value) {
+	for (auto position : positions) {
+		vector[position] = value;
+	}
+}
+
+} //namespace utility
+
+} //namespace mrmc
+
+#endif /* VECTOR_H_ */