Merge with master.

CMakeLists.txt

@@ -87,9 +87,8 @@ else(CLANG)
 	# As CLANG is not set as a variable, we need to set it in case we have not matched another compiler.
 	set (CLANG ON)
     # Set standard flags for clang
-    set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
-    # TODO: activate -Werror asap
-    set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE")
+    set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4")
+    set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE")
     
     # Turn on popcnt instruction if desired (yes by default)
     if (USE_POPCNT)
@@ -240,9 +239,9 @@ configure_file (
   "${PROJECT_BINARY_DIR}/storm-config.h"
 )
 
-add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab
+add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm -v --fix-deadlocks ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab
 						DEPENDS storm)
-add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-tests
+add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-tests -v --fix-deadlocks 
 						DEPENDS storm-tests)
 						
 set (CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams)

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/adapters/GmmxxAdapter.h

@@ -23,7 +23,7 @@ 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.
+	 * @return A pointer to a row-major sparse matrix in gmm++ format.
 	 */
 	template<class T>
 	static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SparseMatrix<T> const& matrix) {
@@ -31,15 +31,16 @@ public:
 		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>(matrix.rowCount, matrix.rowCount);
+		gmm::csr_matrix<T>* result = new gmm::csr_matrix<T>(matrix.rowCount, matrix.colCount);
 
 		// Copy Row Indications
-		std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), std::back_inserter(result->jc));
+		std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), result->jc.begin());
 		// Copy Columns Indications
 		result->ir.resize(realNonZeros);
-		std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), std::back_inserter(result->ir));
+		std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), result->ir.begin());
 		// And do the same thing with the actual values.
-		std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), std::back_inserter(result->pr));
+		result->pr.resize(realNonZeros);
+		std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), result->pr.begin());
 
 		LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format.");
 

src/exceptions/BaseException.h

@@ -28,7 +28,11 @@ class BaseException : public std::exception {
 		}
 		
 		virtual const char* what() const throw() {
-			return this->stream.str().c_str();
+			std::string errorString = this->stream.str();
+			char* result = new char[errorString.size() + 1];
+			result[errorString.size()] = '\0';
+			std::copy(errorString.begin(), errorString.end(), result);
+			return result;
 		}
 	
 	private:

src/exceptions/InvalidAccessException.h

@@ -0,0 +1,19 @@
+#ifndef STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_
+#define STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_
+
+#include "src/exceptions/BaseException.h"
+
+namespace storm {
+
+namespace exceptions {
+
+/*! 
+ * @brief This exception is thrown when a function is used/accessed that is forbidden to use (e.g. Copy Constructors)
+ */
+STORM_EXCEPTION_DEFINE_NEW(InvalidAccessException)
+
+} // namespace exceptions
+
+} // namespace storm
+
+#endif // STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_

src/modelChecker/DtmcPrctlModelChecker.h

@@ -31,6 +31,7 @@ class DtmcPrctlModelChecker;
 #include "src/models/Dtmc.h"
 #include "src/storage/BitVector.h"
 #include "src/exceptions/InvalidPropertyException.h"
+#include "src/utility/Vector.h"
 #include <vector>
 
 #include "log4cplus/logger.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/modelChecker/GmmxxDtmcPrctlModelChecker.h

@@ -18,6 +18,7 @@
 #include "src/utility/Settings.h"
 #include "src/adapters/GmmxxAdapter.h"
 #include "src/exceptions/InvalidPropertyException.h"
+#include "src/storage/JacobiDecomposition.h"
 
 #include "gmm/gmm_matrix.h"
 #include "gmm/gmm_iter_solvers.h"
@@ -128,7 +129,8 @@ public:
 		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
 
 		// Only try to solve system if there are states for which the probability is unknown.
-		if (maybeStates.getNumberOfSetBits() > 0) {
+		uint_fast64_t mayBeStatesSetBitCount = maybeStates.getNumberOfSetBits();
+		if (mayBeStatesSetBitCount > 0) {
 			// Now we can eliminate the rows and columns from the original transition probability matrix.
 			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
 			// Converting the matrix from the fixpoint notation to the form needed for the equation
@@ -142,11 +144,11 @@ public:
 			// 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<Type> x(maybeStates.getNumberOfSetBits(), Type(0.5));
+			std::vector<Type> x(mayBeStatesSetBitCount, Type(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<Type> b(maybeStates.getNumberOfSetBits());
+			std::vector<Type> b(mayBeStatesSetBitCount);
 			this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &b);
 
 			// Solve the corresponding system of linear equations.
@@ -259,7 +261,8 @@ public:
 
 		// Check whether there are states for which we have to compute the result.
 		storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates;
-		if (maybeStates.getNumberOfSetBits() > 0) {
+		const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
+		if (maybeStatesSetBitCount > 0) {
 			// Now we can eliminate the rows and columns from the original transition probability matrix.
 			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
 			// Converting the matrix from the fixpoint notation to the form needed for the equation
@@ -272,10 +275,10 @@ public:
 
 			// Initialize the x vector with 1 for each element. This is the initial guess for
 			// the iterative solvers.
-			std::vector<Type> x(maybeStates.getNumberOfSetBits(), storm::utility::constGetOne<Type>());
+			std::vector<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>());
 
 			// Prepare the right-hand side of the equation system.
-			std::vector<Type>* b = new std::vector<Type>(maybeStates.getNumberOfSetBits());
+			std::vector<Type>* b = new std::vector<Type>(maybeStatesSetBitCount);
 			if (this->getModel().hasTransitionRewards()) {
 				// If a transition-based reward model is available, we initialize the right-hand
 				// side to the vector resulting from summing the rows of the pointwise product
@@ -289,7 +292,7 @@ public:
 					// as well. As the state reward vector contains entries not just for the states
 					// that we still consider (i.e. maybeStates), we need to extract these values
 					// first.
-					std::vector<Type>* subStateRewards = new std::vector<Type>(maybeStates.getNumberOfSetBits());
+					std::vector<Type>* subStateRewards = new std::vector<Type>(maybeStatesSetBitCount);
 					storm::utility::setVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewards());
 					gmm::add(*subStateRewards, *b);
 					delete subStateRewards;
@@ -444,6 +447,64 @@ private:
 			LOG4CPLUS_WARN(logger, "Iterative solver did not converge.");
 		}
 	}
+
+	/*!
+	 * Solves the linear equation system Ax=b with the given parameters
+	 * using the Jacobi Method and therefor the Jacobi Decomposition of A.
+	 *
+	 * @param A The matrix A specifying the coefficients of the linear equations.
+	 * @param x The vector x for which to solve the equations. The initial value of the elements of
+	 * this vector are used as the initial guess and might thus influence performance and convergence.
+	 * @param b The vector b specifying the values on the right-hand-sides of the equations.
+	 * @return The solution of the system of linear equations in form of the elements of the vector
+	 * x.
+	 */
+	void solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b) const {
+		// Get the settings object to customize linear solving.
+		storm::settings::Settings* s = storm::settings::instance();
+
+		double precision = s->get<double>("precision");
+		if (precision <= 0) {
+			LOG4CPLUS_ERROR(logger, "Selected precision for linear equation solving must be strictly greater than zero for Jacobi method.");
+		}
+			
+		// Get a Jacobi Decomposition of the Input Matrix A
+		storm::storage::JacobiDecomposition<Type>* jacobiDecomposition = A.getJacobiDecomposition();
+
+		// Convert the Diagonal matrix to GMM format
+		gmm::csr_matrix<Type>* gmmxxDiagonalInverted = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(jacobiDecomposition->getJacobiDInv());
+		// Convert the LU Matrix to GMM format
+		gmm::csr_matrix<Type>* gmmxxLU = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(jacobiDecomposition->getJacobiLU());
+
+		delete jacobiDecomposition;
+
+		LOG4CPLUS_INFO(logger, "Starting iterative Jacobi Solver.");
+		
+		// x_(k + 1) = D^-1 * (b  - R * x_k)
+		std::vector<Type>* xNext = new std::vector<Type>(x.size());
+		const std::vector<Type>* xCopy = xNext;
+		std::vector<Type>* xCurrent = &x;
+
+		uint_fast64_t iterationCount = 0;
+		do {
+			// R * x_k -> xCurrent
+			gmm::mult(*gmmxxLU, *xCurrent, *xNext);
+			// b - R * x_k
+			gmm::add(b, gmm::scaled(*xNext, -1.0), *xNext);
+			// D^-1 * (b - R * x_k)
+			gmm::mult(*gmmxxDiagonalInverted, *xNext, *xNext);
+			
+			std::vector<Type>* swap = xNext;
+			xNext = xCurrent;
+			xCurrent = swap;
+
+			++iterationCount;
+		} while (gmm::vect_norminf(*xCurrent) > precision);
+
+		delete xCopy;
+
+		LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterationCount << " iterations.");
+	}
 };
 
 } //namespace modelChecker

src/models/AbstractModel.cpp

@@ -13,13 +13,13 @@
  *	@return Output stream os.
  */
 std::ostream& storm::models::operator<<(std::ostream& os, storm::models::ModelType const type) {
-    switch (type) {
-        case storm::models::Unknown: os << "Unknown"; break;
-        case storm::models::DTMC: os << "DTMC"; break;
-        case storm::models::CTMC: os << "CTMC"; break;
-        case storm::models::MDP: os << "MDP"; break;
-        case storm::models::CTMDP: os << "CTMDP"; break;
-        default: os << "Invalid ModelType"; break;
-    }
-    return os;
+	switch (type) {
+		case storm::models::Unknown: os << "Unknown"; break;
+		case storm::models::DTMC: os << "DTMC"; break;
+		case storm::models::CTMC: os << "CTMC"; break;
+		case storm::models::MDP: os << "MDP"; break;
+		case storm::models::CTMDP: os << "CTMDP"; break;
+		default: os << "Invalid ModelType"; break;
+	}
+	return os;
 }

src/models/AbstractModel.h

@@ -24,7 +24,7 @@ std::ostream& operator<<(std::ostream& os, ModelType const type);
  *	This is base class defines a common interface for all models to identify
  *	their type and obtain the special model.
  */
-class AbstractModel {
+class AbstractModel: public std::enable_shared_from_this<AbstractModel> {
 
 	public:
 		/*!
@@ -44,7 +44,7 @@ class AbstractModel {
 		 */
 		template <typename Model>
 		std::shared_ptr<Model> as() {
-			return std::dynamic_pointer_cast<Model>(std::shared_ptr<AbstractModel>(this));
+			return std::dynamic_pointer_cast<Model>(shared_from_this());
 		}
 		
 		/*!

src/models/Dtmc.h

@@ -53,6 +53,12 @@ public:
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
 		}
+		if (this->transitionRewardMatrix != nullptr) {
+			if (!this->transitionRewardMatrix->isSubmatrixOf(*(this->probabilityMatrix))) {
+				LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
+				throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions.";
+			}
+		}
 	}
 
 	//! Copy Constructor
@@ -66,10 +72,7 @@ public:
 		if (dtmc.backwardTransitions != nullptr) {
 			this->backwardTransitions = new storm::models::GraphTransitions<T>(*dtmc.backwardTransitions);
 		}
-		if (!this->checkValidityOfProbabilityMatrix()) {
-			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
-			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
-		}
+		// no checks here, as they have already been performed for dtmc.
 	}
 
 	//! Destructor
@@ -215,13 +218,20 @@ private:
 
 		if (this->probabilityMatrix->getRowCount() != this->probabilityMatrix->getColumnCount()) {
 			// not square
+			LOG4CPLUS_ERROR(logger, "Probability matrix is not square.");
 			return false;
 		}
 
 		for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) {
 			T sum = this->probabilityMatrix->getRowSum(row);
-			if (sum == 0) return false;
-			if (std::abs(sum - 1) > precision) return false;
+			if (sum == 0) {
+				LOG4CPLUS_ERROR(logger, "Row " << row << " has sum 0");
+				return false;
+			}
+			if (std::abs(sum - 1) > precision) {
+				LOG4CPLUS_ERROR(logger, "Row " << row << " has sum " << sum);
+				return false;
+			}
 		}
 		return true;
 	}

src/parser/AutoParser.cpp

@@ -5,7 +5,7 @@
 
 #include "src/exceptions/WrongFileFormatException.h"
 #include "src/models/AbstractModel.h"
-#include "src/parser/DtmcParser.h"
+#include "src/parser/DeterministicModelParser.h"
 #include "src/parser/MdpParser.h"
 
 namespace storm {
@@ -27,15 +27,18 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con
 	// Do actual parsing
 	switch (type) {
 		case storm::models::DTMC: {
-			DtmcParser* parser = new DtmcParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-			this->model = parser->getDtmc();
+			DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+			this->model = parser.getDtmc();
 			break;
 		}
-		case storm::models::CTMC:
+		case storm::models::CTMC: {
+			DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+			this->model = parser.getCtmc();
 			break;
+		}
 		case storm::models::MDP: {
-			MdpParser* parser = new MdpParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-			this->model = parser->getMdp();
+			MdpParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+			this->model = parser.getMdp();
 			break;
 		}
 		case storm::models::CTMDP:
@@ -43,7 +46,10 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con
 		default: ;  // Unknown
 	}
 
-	if (!this->model) std::cout << "model is still null" << std::endl;
+	
+	if (!this->model) {
+		LOG4CPLUS_WARN(logger, "Model is still null.");
+	}
 }
 
 storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) {

src/parser/AutoParser.h

@@ -14,7 +14,7 @@ namespace parser {
 /*!
  *	@brief Checks the given files and parses the model within these files.
  *
- *	This parser analyzes the format hitn in the first line of the transition
+ *	This parser analyzes the format hint in the first line of the transition
  *	file. If this is a valid format, it will use the parser for this format,
  *	otherwise it will throw an exception.
  *

src/parser/DtmcParser.cpp → src/parser/DeterministicModelParser.cpp

@@ -1,11 +1,11 @@
 /*
- * DtmcParser.cpp
+ * DeterministicModelParser.cpp
  *
  *  Created on: 19.12.2012
  *      Author: thomas
  */
 
-#include "src/parser/DtmcParser.h"
+#include "src/parser/DeterministicModelParser.h"
 
 #include <string>
 #include <vector>
@@ -27,25 +27,29 @@ namespace parser {
  * @param stateRewardFile String containing the location of the state reward file (...srew)
  * @param transitionRewardFile String containing the location of the transition reward file (...trew)
  */
-DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+DeterministicModelParser::DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
 		std::string const & stateRewardFile, std::string const & transitionRewardFile) {
 	storm::parser::DeterministicSparseTransitionParser tp(transitionSystemFile);
-	uint_fast64_t stateCount = tp.getMatrix()->getRowCount();
+	this->transitionSystem = tp.getMatrix();
 	
-	std::shared_ptr<std::vector<double>> stateRewards = nullptr;
-	std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards = nullptr;
+	uint_fast64_t stateCount = this->transitionSystem->getRowCount();
 
 	storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
+	this->labeling = lp.getLabeling();
+	
+	this->stateRewards = nullptr;
+	this->transitionRewards = nullptr;
+
 	if (stateRewardFile != "") {
 		storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile);
-		stateRewards = srp.getStateRewards();
+		this->stateRewards = srp.getStateRewards();
 	}
 	if (transitionRewardFile != "") {
 		storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile);
-		transitionRewards = trp.getMatrix();
+		this->transitionRewards = trp.getMatrix();
 	}
-
-	dtmc = std::shared_ptr<storm::models::Dtmc<double>>(new storm::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards));
+	this->dtmc = nullptr;
+	this->ctmc = nullptr;
 }
 
 } /* namespace parser */

src/parser/DeterministicModelParser.h

@@ -0,0 +1,62 @@
+/*
+ * DtmcParser.h
+ *
+ *  Created on: 19.12.2012
+ *      Author: thomas
+ */
+
+#ifndef STORM_PARSER_DETERMINISTICMODELPARSER_H_
+#define STORM_PARSER_DETERMINISTICMODELPARSER_H_
+
+#include "src/parser/Parser.h"
+#include "src/models/Dtmc.h"
+#include "src/models/Ctmc.h"
+
+namespace storm {
+namespace parser {
+
+/*!
+ *	@brief Load label and transition file and return initialized dtmc or ctmc object.
+ *
+ *	@Note This class creates a new Dtmc or Ctmc object that can
+ *	be accessed via getDtmc() or getCtmc(). However, it will not delete this object!
+ *
+ *	@Note The labeling representation in the file may use at most as much nodes as are specified in the transition system.
+ */
+class DeterministicModelParser: public storm::parser::Parser {
+	public:
+		DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
+
+		/*!
+		 *	@brief	Get the parsed dtmc model.
+		 */
+		std::shared_ptr<storm::models::Dtmc<double>> getDtmc() {
+			if (this->dtmc == nullptr) {
+				this->dtmc = std::shared_ptr<storm::models::Dtmc<double>>(new storm::models::Dtmc<double>(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards));
+			}
+			return this->dtmc;
+		}
+		/*!
+		 *	@brief	Get the parsed ctmc model.
+		 */
+		std::shared_ptr<storm::models::Ctmc<double>> getCtmc() {
+			if (this->ctmc == nullptr) {
+				this->ctmc = std::shared_ptr<storm::models::Ctmc<double>>(new storm::models::Ctmc<double>(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards));
+			}
+			return this->ctmc;
+		}
+
+	private:
+		std::shared_ptr<storm::storage::SparseMatrix<double>> transitionSystem;
+		std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling;
+		std::shared_ptr<std::vector<double>> stateRewards;
+		std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards;
+	
+		std::shared_ptr<storm::models::Dtmc<double>> dtmc;
+		std::shared_ptr<storm::models::Ctmc<double>> ctmc;
+};
+
+} /* namespace parser */
+} /* namespace storm */
+#endif /* STORM_PARSER_DETERMINISTICMODELPARSER_H_ */

src/parser/DeterministicSparseTransitionParser.cpp

@@ -44,8 +44,8 @@ namespace parser {
  *	@param buf Data to scan. Is expected to be some char array.
  *	@param maxnode Is set to highest id of all nodes.
  */
-uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& maxnode) {
-	uint_fast64_t non_zero = 0;
+uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode) {
+	uint_fast64_t nonZeroEntryCount = 0;
 
 	/*
 	 *	Check file header and extract number of transitions.
@@ -63,47 +63,75 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas
 		return 0;
 	}
 	buf += 12;  // skip "TRANSITIONS "
-	if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0;
+	if ((nonZeroEntryCount = strtol(buf, &buf, 10)) == 0) return 0;
 
-	/*
-	 *	Check all transitions for non-zero diagonal entrys.
-	 */
-	uint_fast64_t row, lastrow = 0, col;
-	double val;
-	maxnode = 0;
-	while (buf[0] != '\0') {
-		/*
-		 *	Read row and column.
-		 */
-		row = checked_strtol(buf, &buf);
-		col = checked_strtol(buf, &buf);
-		/*
-		 *	Check if one is larger than the current maximum id.
-		 */
-		if (row > maxnode) maxnode = row;
-		if (col > maxnode) maxnode = col;
-		/*
-		 *	Check if a node was skipped, i.e. if a node has no outgoing
-		 *	transitions. If so, increase non_zero, as the second pass will
-		 *	either throw an exception (in this case, it doesn't matter
-		 *	anyway) or add a self-loop (in this case, we'll need the
-		 *	additional transition).
-		 */
-		if (lastrow < row-1) non_zero += row - lastrow - 1;
-		lastrow = row;
-		/*
-		 *	Read probability of this transition.
-		 *	Check, if the value is a probability, i.e. if it is between 0 and 1.
-		 */
-		val = checked_strtod(buf, &buf);
-		if ((val < 0.0) || (val > 1.0)) {
-			LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
-			return 0;
-		}
-		buf = trimWhitespaces(buf);
-	}
+    /*
+     * Check all transitions for non-zero diagonal entries and deadlock states.
+     */
+    int_fast64_t row, lastRow = -1, col;
+    bool rowHadDiagonalEntry = false;
+    double val;
+    maxnode = 0;
+    while (buf[0] != '\0') {
+            /*
+             *      Read row and column.
+             */
+            row = checked_strtol(buf, &buf);
+            col = checked_strtol(buf, &buf);
+
+            /*
+             * 		If we have switched to the next row, we need to clear the information about
+             * 		the diagonal entry.
+             */
+            if (row != lastRow) {
+            	/*
+            	 * If the last row did have transitions, but no diagonal element, we need to insert
+            	 * it as well.
+            	 */
+            	if (!rowHadDiagonalEntry && lastRow != -1) {
+            		++nonZeroEntryCount;
+            	}
+            	rowHadDiagonalEntry = false;
+            }
 
-	return non_zero;
+            if (row == col) {
+            	rowHadDiagonalEntry = true;
+            }
+
+            /*
+             *      Check if one is larger than the current maximum id.
+             */
+            if (row > maxnode) maxnode = row;
+            if (col > maxnode) maxnode = col;
+
+            /*
+             *      Check if a node was skipped, i.e. if a node has no outgoing
+             *      transitions. If so, increase non_zero, as the second pass will
+             *      either throw an exception (in this case, it doesn't matter
+             *      anyway) or add a self-loop (in this case, we'll need the
+             *      additional transition).
+             */
+            if (lastRow < row - 1) {
+            	nonZeroEntryCount += row - lastRow - 1;
+            }
+            lastRow = row;
+            /*
+             *      Read probability of this transition.
+             *      Check, if the value is a probability, i.e. if it is between 0 and 1.
+             */
+            val = checked_strtod(buf, &buf);
+            if ((val < 0.0) || (val > 1.0)) {
+                    LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
+                    return 0;
+            }
+            buf = trimWhitespaces(buf);
+    }
+
+    if (!rowHadDiagonalEntry) {
+    	++nonZeroEntryCount;
+    }
+
+    return nonZeroEntryCount;
 }
 
 
@@ -116,7 +144,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas
  *	@return a pointer to the created sparse matrix.
  */
 
-DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename)
+DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing)
 	: matrix(nullptr) {
 	/*
 	 *	Enforce locale where decimal point is '.'.
@@ -132,12 +160,12 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	/*
 	 *	Perform first pass, i.e. count entries that are not zero.
 	 */
-	uint_fast64_t maxnode;
-	uint_fast64_t non_zero = this->firstPass(file.data, maxnode);
+	int_fast64_t maxStateId;
+	uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId);
 	/*
 	 *	If first pass returned zero, the file format was wrong.
 	 */
-	if (non_zero == 0) {
+	if (nonZeroEntryCount == 0) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format.");
 		throw storm::exceptions::WrongFileFormatException();
 	}
@@ -162,21 +190,22 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	 *	Creating matrix here.
 	 *	The number of non-zero elements is computed by firstPass().
 	 */
-	LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
-	this->matrix = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(maxnode + 1));
-	if (this->matrix == NULL) {
-		LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
+	LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << ".");
+	this->matrix = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(maxStateId + 1));
+	if (this->matrix == nullptr) {
+		LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << ".");
 		throw std::bad_alloc();
 	}
-	this->matrix->initialize(non_zero);
+	this->matrix->initialize(nonZeroEntryCount);
 
-	uint_fast64_t row, lastrow = 0, col;
+	int_fast64_t row, lastRow = -1, col;
 	double val;
 	bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks");
 	bool hadDeadlocks = false;
+	bool rowHadDiagonalEntry = false;
 
 	/*
-	 *	Read all transitions from file. Note that we assume, that the
+	 *	Read all transitions from file. Note that we assume that the
 	 *	transitions are listed in canonical order, otherwise this will not
 	 *	work, i.e. the values in the matrix will be at wrong places.
 	 */
@@ -188,24 +217,58 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 		col = checked_strtol(buf, &buf);
 		val = checked_strtod(buf, &buf);
 
+		if (row != lastRow) {
+			/*
+			 * 	If the previous row did not have a diagonal entry, we need to insert it.
+			 */
+			if (!rowHadDiagonalEntry && lastRow != -1) {
+				this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
+			}
+
+			rowHadDiagonalEntry = false;
+		}
+
 		/*
-		 *	Check if we skipped a node, i.e. if a node does not have any
+		 *	Check if we skipped a state entirely, i.e. a state does not have any
 		 *	outgoing transitions.
 		 */
-		for (uint_fast64_t node = lastrow + 1; node < row; node++) {
-			hadDeadlocks = true;
-			if (fixDeadlocks) {
-				this->matrix->addNextValue(node, node, 1);
-				LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
-			} else {
-				LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
+		if ((lastRow + 1) < row) {
+			for (int_fast64_t state = lastRow + 1; state < row; ++state) {
+				hadDeadlocks = true;
+				if (fixDeadlocks) {
+					this->matrix->addNextValue(state, state, storm::utility::constGetOne<double>());
+					LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << state << " has no outgoing transitions. A self-loop was inserted.");
+				} else {
+					LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << state << " has no outgoing transitions.");
+				}
 			}
 		}
-		lastrow = row;
+
+		// Insert the missing diagonal value here, because the input skipped it.
+		if (col > row && !rowHadDiagonalEntry) {
+			if (insertDiagonalEntriesIfMissing) {
+				this->matrix->addNextValue(row, row, storm::utility::constGetZero<double>());
+			}
+			rowHadDiagonalEntry = true;
+		}
+
+		/*
+		 * Check if the transition is a self-loop
+		 */
+		if (row == col) {
+			rowHadDiagonalEntry = true;
+		}
+
+		lastRow = row;
 
 		this->matrix->addNextValue(row, col, val);
 		buf = trimWhitespaces(buf);
 	}
+
+	if (!rowHadDiagonalEntry) {
+		this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
+	}
+
 	if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
 
 	/*

src/parser/DeterministicSparseTransitionParser.h

@@ -17,7 +17,7 @@ namespace parser {
  */
 class DeterministicSparseTransitionParser : public Parser {
 	public:
-		DeterministicSparseTransitionParser(std::string const &filename);
+		DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true);
 		
 		std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
 			return this->matrix;
@@ -26,7 +26,7 @@ class DeterministicSparseTransitionParser : public Parser {
 	private:
 		std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
 		
-		uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode);
+		uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode);
 	
 };
 		

src/parser/DtmcParser.h

@@ -1,40 +0,0 @@
-/*
- * DtmcParser.h
- *
- *  Created on: 19.12.2012
- *      Author: thomas
- */
-
-#ifndef STORM_PARSER_DTMCPARSER_H_
-#define STORM_PARSER_DTMCPARSER_H_
-
-#include "src/parser/Parser.h"
-#include "src/models/Dtmc.h"
-
-namespace storm {
-namespace parser {
-
-/*!
- *	@brief Load label and transition file and return initialized dtmc object
- *
- *	@Note This class creates a new Dtmc object that can
- *	be accessed via getDtmc(). However, it will not delete this object!
- *
- *	@Note The labeling representation in the file may use at most as much nodes as are specified in the dtmc.
- */
-class DtmcParser: public storm::parser::Parser {
-public:
-	DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile,
-			std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
-
-	std::shared_ptr<storm::models::Dtmc<double>> getDtmc() {
-		return this->dtmc;
-	}
-
-private:
-	std::shared_ptr<storm::models::Dtmc<double>> dtmc;
-};
-
-} /* namespace parser */
-} /* namespace storm */
-#endif /* STORM_PARSER_DTMCPARSER_H_ */

src/parser/NonDeterministicSparseTransitionParser.cpp

@@ -49,7 +49,7 @@ namespace parser {
  *	@param maxnode Is set to highest id of all nodes.
  *	@return The number of non-zero elements.
  */
-uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode) {
+uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
 	/*
 	 *	Check file header and extract number of transitions.
 	 */
@@ -77,8 +77,8 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_
 	/*
 	 *	Read all transitions.
 	 */
-	uint_fast64_t source, target;
-	uint_fast64_t lastsource = 0;
+	int_fast64_t source, target;
+	int_fast64_t lastsource = -1;
 	uint_fast64_t nonzero = 0;
 	double val;
 	choices = 0;
@@ -97,6 +97,7 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_
 		choices++;
 		if (source > lastsource + 1) {
 			nonzero += source - lastsource - 1;
+			choices += source - lastsource - 1;
 			parsed_nonzero += source - lastsource - 1;
 		}
 		lastsource = source;
@@ -169,7 +170,8 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 	/*
 	 *	Perform first pass, i.e. obtain number of columns, rows and non-zero elements.
 	 */
-	uint_fast64_t maxnode, choices;
+	int_fast64_t maxnode;
+	uint_fast64_t choices;
 	uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode);
 
 	/*
@@ -217,7 +219,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 	/*
 	 *	Parse file content.
 	 */
-	uint_fast64_t source, target, lastsource = 0;
+	int_fast64_t source, target, lastsource = -1;
 	uint_fast64_t curRow = 0;
 	std::string choice;
 	double val;
@@ -240,7 +242,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 		 *	outgoing transitions. If so, insert a self-loop.
 		 *	Also add self-loops to rowMapping.
 		 */
-		for (uint_fast64_t node = lastsource + 1; node < source; node++) {
+		for (int_fast64_t node = lastsource + 1; node < source; node++) {
 			hadDeadlocks = true;
 			if (fixDeadlocks) {
 				this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, "")));

src/parser/NonDeterministicSparseTransitionParser.h

@@ -35,7 +35,7 @@ class NonDeterministicSparseTransitionParser : public Parser {
 		std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
 		std::shared_ptr<RowMapping> rowMapping;
 		
-		uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode);
+		uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode);
 	
 };
 		

src/storage/BitVector.h

@@ -69,13 +69,17 @@ public:
 		 * Returns the index of the current bit that is set to true.
 		 * @return The index of the current bit that is set to true.
 		 */
-		uint_fast64_t operator*() const { return currentIndex; }
+		uint_fast64_t operator*() const {
+			return currentIndex;
+		}
 
 		/*!
 		 * Compares the iterator with another iterator to determine whether
 		 * the iteration process has reached the end.
 		 */
-		bool operator!=(const constIndexIterator& rhs) const { return currentIndex != rhs.currentIndex; }
+		bool operator!=(const constIndexIterator& rhs) const {
+			return currentIndex != rhs.currentIndex;
+		}
 	private:
 
 		/*! The bit vector to search for set bits. */
@@ -383,11 +387,11 @@ public:
 	 * Returns the number of bits that are set (to one) in this bit vector.
 	 * @return The number of bits that are set (to one) in this bit vector.
 	 */
-	uint_fast64_t getNumberOfSetBits() {
+	uint_fast64_t getNumberOfSetBits() const {
 		return getNumberOfSetBitsBeforeIndex(bucketCount << 6);
 	}
 
-	uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) {
+	uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) const {
 		uint_fast64_t result = 0;
 		// First, count all full buckets.
 		uint_fast64_t bucket = index >> 6;
@@ -433,7 +437,7 @@ public:
 	/*!
 	 * Retrieves the number of bits this bit vector can store.
 	 */
-	uint_fast64_t getSize() {
+	uint_fast64_t getSize() const {
 		return bitCount;
 	}
 
@@ -441,7 +445,7 @@ public:
 	 * Returns the size of the bit vector in memory measured in bytes.
 	 * @return The size of the bit vector in memory measured in bytes.
 	 */
-	uint_fast64_t getSizeInMemory() {
+	uint_fast64_t getSizeInMemory() const {
 		return sizeof(*this) + sizeof(uint_fast64_t) * bucketCount;
 	}
 
@@ -459,6 +463,20 @@ public:
 		return endIterator;
 	}
 
+	/*!
+	 * Returns a string representation of the bit vector.
+	 */
+	std::string toString() const {
+		std::stringstream result;
+		result << "bit vector(" << this->getNumberOfSetBits() << ") [";
+		for (auto index : *this) {
+			result << index << " ";
+		}
+		result << "]";
+
+		return result.str();
+	}
+
 private:
 
 	/*!

src/storage/JacobiDecomposition.h

@@ -6,6 +6,8 @@
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
 
+#include "src/exceptions/InvalidAccessException.h"
+
 extern log4cplus::Logger logger;
 
 namespace storm {
@@ -76,7 +78,9 @@ private:
 	 * The copy constructor is disabled for this class.
 	 */
 	//JacobiDecomposition(const JacobiDecomposition<T>& that) = delete; // not possible in VS2012
-	JacobiDecomposition(const JacobiDecomposition<T>& that) {}
+	JacobiDecomposition(const JacobiDecomposition<T>& that) {
+		throw storm::exceptions::InvalidAccessException() << "The copy constructor of JacobiDecomposition is explicitly disabled.";
+	}
 
 	/*!
 	 * Pointer to the LU Matrix

src/storage/SparseMatrix.h

@@ -25,10 +25,14 @@
 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 {
 namespace storage {
 
 /*!
@@ -43,6 +47,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
@@ -91,7 +96,8 @@ public:
 	 * Constructs a square sparse matrix object with the given number rows
 	 * @param size The number of rows and cols in the matrix
 	 */
-	SparseMatrix(uint_fast64_t size) : rowCount(size), colCount(size), nonZeroEntryCount(0),
+	SparseMatrix(uint_fast64_t size)
+			: rowCount(size), colCount(size), nonZeroEntryCount(0),
 			  internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { }
 
 	//! Copy Constructor
@@ -114,12 +120,12 @@ public:
 				LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage.");
 				throw std::bad_alloc();
 			} else {
-				std::copy(ssm.valueStorage.begin(), ssm.valueStorage.end(), std::back_inserter(valueStorage));
+				std::copy(ssm.valueStorage.begin(), ssm.valueStorage.end(), valueStorage.begin());
 
 				// The elements that are not of the value type but rather the
 				// index type may be copied directly.
-				std::copy(ssm.columnIndications.begin(), ssm.columnIndications.end(), std::back_inserter(columnIndications));
-				std::copy(ssm.rowIndications.begin(), ssm.rowIndications.end(), std::back_inserter(rowIndications));
+				std::copy(ssm.columnIndications.begin(), ssm.columnIndications.end(), columnIndications.begin());
+				std::copy(ssm.rowIndications.begin(), ssm.rowIndications.end(), rowIndications.begin());
 			}
 		}
 	}
@@ -318,7 +324,6 @@ public:
 			throw storm::exceptions::OutOfRangeException("Trying to add a value at illegal position.");
 		}
 
-		
 		// If we switched to another row, we have to adjust the missing
 		// entries in the row_indications array.
 		if (row != lastRow) {
@@ -662,8 +667,9 @@ public:
 		uint_fast64_t rowEnd = rowIndications[row + 1];
 
 		if (rowStart >= rowEnd) {
-			LOG4CPLUS_ERROR(logger, "The row " << row << " can not be made absorbing, no state in row, would have to recreate matrix!");
-			throw storm::exceptions::InvalidStateException("A row can not be made absorbing, no state in row, would have to recreate matrix!");
+			this->print();
+			LOG4CPLUS_ERROR(logger, "Cannot make row absorbing, because there is no entry in this row.");
+			throw storm::exceptions::InvalidStateException("Cannot make row absorbing, because there is no entry in this row.");
 		}
 		uint_fast64_t pseudoDiagonal = row % colCount;
 
@@ -793,22 +799,29 @@ public:
 	/*!
 	 * Inverts all elements on the diagonal, i.e. sets the diagonal values to 1 minus their previous
 	 * value.
+	 * Requires the matrix to contain each diagonal element AND to be square!
 	 */
 	void invertDiagonal() {
 		if (this->getRowCount() != this->getColumnCount()) {
 			throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!";
 		}
-		T one(1);
+		T one = storm::utility::constGetOne<T>();
+		bool foundRow;
 		for (uint_fast64_t row = 0; row < rowCount; ++row) {
 			uint_fast64_t rowStart = rowIndications[row];
 			uint_fast64_t rowEnd = rowIndications[row + 1];
+			foundRow = false;
 			while (rowStart < rowEnd) {
 				if (columnIndications[rowStart] == row) {
 					valueStorage[rowStart] = one - valueStorage[rowStart];
+					foundRow = true;
 					break;
 				}
 				++rowStart;
 			}
+			if (!foundRow) {
+				throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to contain all diagonal entries!";
+			}
 		}
 	}
 
@@ -841,9 +854,13 @@ public:
 		SparseMatrix<T> *resultDinv = new SparseMatrix<T>(rowCount);
 		// no entries apart from those on the diagonal
 		resultDinv->initialize(0);
+
+		// constant 1 for diagonal inversion
+		T constOne = storm::utility::constGetOne<T>();
+
 		// copy diagonal entries to other matrix
 		for (int i = 0; i < rowCount; ++i) {
-			resultDinv->addNextValue(i, i, resultLU->getValue(i, i));
+			resultDinv->addNextValue(i, i, constOne / resultLU->getValue(i, i));
 			resultLU->getValue(i, i) = storm::utility::constGetZero<T>();
 		}
 
@@ -883,6 +900,18 @@ public:
 		return result;
 	}
 
+	T getRowVectorProduct(uint_fast64_t row, std::vector<T>& vector) {
+		T result = storm::utility::constGetZero<T>();;
+		auto valueIterator = valueStorage.begin() + rowIndications[row];
+		const auto valueIteratorEnd = valueStorage.begin() + rowIndications[row + 1];
+		auto columnIterator = columnIndications.begin() + rowIndications[row];
+		const auto columnIteratorEnd = columnIndications.begin() + rowIndications[row + 1];
+		for (; valueIterator != valueIteratorEnd; ++valueIterator, ++columnIterator) {
+			result += *valueIterator * vector[*columnIterator];
+		}
+		return result;
+	}
+
 	/*!
 	 * Returns the size of the matrix in memory measured in bytes.
 	 * @return The size of the matrix in memory measured in bytes.
@@ -954,13 +983,32 @@ public:
 		return sum;
 	}
 
-	void print() const {
-		std::cout << "entries: ----------------------------" << 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;
+	/*!
+	 *	@brief Checks if it is a submatrix of the given matrix.
+	 *
+	 *	A matrix A is a submatrix of B if a value in A is only nonzero, if
+	 *	the value in B at the same position is also nonzero. Furthermore, A
+	 *	and B have to have the same size.
+	 *	@param matrix Matrix to check against.
+	 *	@return True iff this is a submatrix of matrix.
+	 */
+	bool isSubmatrixOf(SparseMatrix<T> const & matrix) const {
+		if (this->getRowCount() != matrix.getRowCount()) return false;
+		if (this->getColumnCount() != matrix.getColumnCount()) return false;
+
+		for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) {
+			for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem, ++elem2) {
+				if (columnIndications[elem] < matrix.columnIndications[elem2]) return false;
 			}
 		}
+		return true;
+	}
+
+	void print() const {
+		std::cout << "entries in (" << rowCount << "x" << colCount << " matrix):" << std::endl;
+		std::cout << rowIndications << std::endl;
+		std::cout << columnIndications << std::endl;
+		std::cout << valueStorage << std::endl;
 	}
 
 private:

src/storm.cpp

@@ -103,13 +103,11 @@ bool parseOptions(const int argc, const char* argv[]) {
 	} catch (storm::exceptions::InvalidSettingsException& e) {
 		std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
 		std::cout << std::endl << storm::settings::help;
-		delete s;
 		return false;
 	}
 	
 	if (s->isSet("help")) {
 		std::cout << storm::settings::help;
-		delete s;
 		return false;
 	}
 	if (s->isSet("test-prctl")) {
@@ -137,9 +135,6 @@ bool parseOptions(const int argc, const char* argv[]) {
  * Function to perform some cleanup.
  */
 void cleanUp() {
-	if (storm::settings::instance() != nullptr) {
-		delete storm::settings::instance();
-	}
 	delete storm::utility::cuddUtilityInstance();
 }
 
@@ -226,9 +221,10 @@ void testChecking() {
 	if (parser.getType() == storm::models::DTMC) {
 		std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
 		dtmc->printModelInformationToStream(std::cout);
+
 		// testCheckingDie(*dtmc);
 		// testCheckingCrowds(*dtmc);
-		testCheckingSynchronousLeader(*dtmc, 5);
+		// testCheckingSynchronousLeader(*dtmc, 4);
 	}
 	else std::cout << "Input is not DTMC" << std::endl;
 }

src/utility/Settings.cpp

@@ -33,6 +33,8 @@ storm::settings::Settings* storm::settings::Settings::inst = nullptr;
 
 std::map< std::pair<std::string, std::string>, std::shared_ptr<bpo::options_description> > storm::settings::Settings::modules;
 
+storm::settings::Destroyer storm::settings::Settings::destroyer;
+
 /*!
  *	The constructor fills the option descriptions, parses the
  *	command line and the config file and puts the option values to
@@ -46,7 +48,7 @@ std::map< std::pair<std::string, std::string>, std::shared_ptr<bpo::options_desc
  *	@param argv should be argv passed to main function
  *	@param filename	either nullptr or name of config file
  */
-Settings::Settings(int const argc, char const * const argv[], char const * const filename) {
+Settings::Settings(int const argc, char const * const argv[], char const * const filename, bool const sloppy) {
 	Settings::binaryName = std::string(argv[0]);
 	try {
 		// Initially fill description objects.
@@ -97,7 +99,9 @@ Settings::Settings(int const argc, char const * const argv[], char const * const
 		this->secondRun(argc, argv, filename);
 
 		// Finalize parsed options, check for specified requirements.
-		bpo::notify(this->vm);
+		if (!sloppy) {
+			bpo::notify(this->vm);
+		}
 		LOG4CPLUS_DEBUG(logger, "Finished loading config.");
 	}
 	catch (bpo::reading_file e) {

src/utility/Settings.h

@@ -27,6 +27,8 @@ namespace settings {
 	
 	namespace bpo = boost::program_options;
 	
+	class Destroyer;
+	
 	/*!
 	 *	@brief	Wrapper around boost::program_options to handle configuration options.
 	 *
@@ -43,8 +45,7 @@ namespace settings {
 	 *	option modules. An option module can be anything that implements the
 	 *	interface specified by registerModule().
 	 */
-	class Settings
-	{
+	class Settings {
 		public:
 		
 			/*!
@@ -57,14 +58,14 @@ namespace settings {
 			}
 		
 			/*!
-			 *	@brief	Get value of string option
+			 *	@brief	Get value of string option.
 			 */
 			inline const std::string& getString(std::string const & name) const {
 				return this->get<std::string>(name);
 			}
 		
 			/*!
-			 *	@brief	Check if an option is set
+			 *	@brief	Check if an option is set.
 			 */
 			inline const bool isSet(std::string const & name) const {
 				return this->vm.count(name) > 0;
@@ -122,13 +123,26 @@ namespace settings {
 			friend std::ostream& help(std::ostream& os);
 			friend std::ostream& helpConfigfile(std::ostream& os);
 			friend Settings* instance();
-			friend Settings* newInstance(int const argc, char const * const argv[], char const * const filename);
+			friend Settings* newInstance(int const argc, char const * const argv[], char const * const filename, bool const sloppy = false);
+			friend Destroyer;
 
 		private:
 			/*!
-			 *	@brief	Constructor.
+			 *	@brief	Private constructor.
+			 *
+			 *	This constructor is private, as noone should be able to create
+			 *	an instance manually, one should always use the
+			 *	newInstance() method.
 			 */
-			Settings(int const argc, char const * const argv[], char const * const filename);
+			Settings(int const argc, char const * const argv[], char const * const filename, bool const sloppy);
+			
+			/*!
+			 *	@brief	Private destructor.
+			 *
+			 *	This destructor should be private, as noone should be able to destroy a singleton.
+			 *	The object is automatically destroyed when the program terminates by the destroyer.
+			 */
+			~Settings() {}
 			
 			/*!
 			 *	@brief	Initialize options_description object.
@@ -174,6 +188,33 @@ namespace settings {
 			 *	@brief	actual instance of this class.
 			 */
  			static Settings* inst;
+ 			
+ 			/*!
+ 			 *	@brief	Destroyer object.
+ 			 */
+ 			static Destroyer destroyer;
+	};
+
+	/*!
+	 *	@brief	Destroyer class for singleton object of Settings.
+	 *
+	 *	The sole purpose of this class is to clean up the singleton object
+	 *	instance of Settings. The Settings class has a static member of this
+	 *	Destroyer type that gets cleaned up when the program terminates. In
+	 *	it's destructor, this object will remove the Settings instance.
+	 */
+	class Destroyer {
+		public:
+			/*!
+			 *	@brief	Destructor.
+			 *
+			 *	Free Settings::inst.
+			 */
+			~Destroyer() {
+				if (Settings::inst != nullptr) {
+					delete Settings::inst;
+				}
+			}
 	};
 	
 	/*!
@@ -200,9 +241,9 @@ namespace settings {
 	 *	@param filename either NULL or name of config file
 	 *	@return The new instance of Settings.
 	 */
-	inline Settings* newInstance(int const argc, char const * const argv[], char const * const filename) {
+	inline Settings* newInstance(int const argc, char const * const argv[], char const * const filename, bool const sloppy) {
 		if (Settings::inst != nullptr) delete Settings::inst;
-		Settings::inst = new Settings(argc, argv, filename);
+		Settings::inst = new Settings(argc, argv, filename, sloppy);
 		return Settings::inst;
 	}
 		

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

test/parser/ParseDtmcTest.cpp

@@ -8,12 +8,12 @@
 
 #include "gtest/gtest.h"
 #include "storm-config.h"
-#include "src/parser/DtmcParser.h"
+#include "src/parser/DeterministicModelParser.h"
 #include "src/utility/IoUtility.h"
 
 TEST(ParseDtmcTest, parseAndOutput) {
-	storm::parser::DtmcParser* dtmcParser;
-	ASSERT_NO_THROW(dtmcParser = new storm::parser::DtmcParser(
+	storm::parser::DeterministicModelParser* dtmcParser;
+	ASSERT_NO_THROW(dtmcParser = new storm::parser::DeterministicModelParser(
 			STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra",
 			STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
 

test/storage/SparseMatrixTest.cpp

@@ -94,6 +94,10 @@ TEST(SparseMatrixTest, Test) {
 		2, 3, 4, 5, 6, 7, 8, 9, 10, 11,
 		14, 15, 16, 17, 18, 19, 20, 21, 22, 23 /* second to last row */
 	};
+	int row_sums[25] = {};
+	for (int i = 0; i < 50; ++i) {
+		row_sums[position_row[i]] += values[i];
+	}
 
 	ASSERT_NO_THROW(ssm->initialize(50));
 	ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Initialized);
@@ -123,6 +127,11 @@ TEST(SparseMatrixTest, Test) {
 	}
 	ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
 
+	// Test Row Sums
+	for (int row = 0; row < 25; ++row) {
+		ASSERT_EQ(row_sums[row], ssm->getRowSum(row));
+	}
+
 	delete ssm;
 }
 

test/storm-tests.cpp

@@ -6,6 +6,9 @@
 #include "log4cplus/consoleappender.h"
 #include "log4cplus/fileappender.h"
 
+#include "src/utility/Settings.h"
+#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h"
+
 log4cplus::Logger logger;
 
 /*!
@@ -25,8 +28,36 @@ void setUpLogging() {
 	// logger.addAppender(consoleLogAppender);
 }
 
-int main(int argc, char** argv) {
+/*!
+ * Function that parses the command line options.
+ * @param argc The argc argument of main().
+ * @param argv The argv argument of main().
+ * @return True iff the program should continue to run after parsing the options.
+ */
+bool parseOptions(int const argc, char const * const argv[]) {
+    storm::settings::Settings* s = nullptr;
+    try {
+        storm::settings::Settings::registerModule<storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>>();
+        s = storm::settings::newInstance(argc, argv, nullptr, true);
+    } catch (storm::exceptions::InvalidSettingsException& e) {
+        std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
+        std::cout << std::endl << storm::settings::help;
+        return false;
+    }
+    
+    if (s->isSet("help")) {
+        std::cout << storm::settings::help;
+        return false;
+    }
+    
+    return true; 
+}
+
+int main(int argc, char* argv[]) {
 	setUpLogging();
+	if (!parseOptions(argc, argv)) {
+		return 0;
+	}
 	std::cout << "STORM Testing Suite" << std::endl;
 	
 	testing::InitGoogleTest(&argc, argv);