Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC/

Conflicts:
	src/modelChecker/DtmcPrctlModelChecker.h

	
NOTE:
	makeRowsAbsorbing of SquareSparseMatrix did not return a value. To
	suppress the warning I added "return false", so that the program
	compiles for me with "-Werror", too.

resources/3rdparty/log4cplus-1.1.0/src/liblog4cplus.0.dylib

@@ -1 +0,0 @@
-liblog4cplus.1.1.0.dylib

resources/3rdparty/log4cplus-1.1.0/src/liblog4cplus.dylib

@@ -1 +0,0 @@
-liblog4cplus.0.dylib

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,19 @@ 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);
+		}
+
+		//FIXME: Had no return value; as I compile with -Werror ATM, build did not work so I added:
+		return false;
+		//(Thomas Heinemann, 06.12.2012)
+	}
+
 	/*!
 	 * 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 +725,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 +763,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 +802,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 +864,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_ */