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

Conflicts:
	src/storage/SparseMatrix.h

CMakeLists.txt

@@ -194,9 +194,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/GmmxxAdapter.h

@@ -34,12 +34,13 @@ public:
 		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/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

src/parser/AtomicPropositionLabelingParser.h

@@ -24,7 +24,7 @@ class AtomicPropositionLabelingParser : Parser {
 		std::shared_ptr<storm::models::AtomicPropositionsLabeling> getLabeling() {
 			return this->labeling;
 		}
-	
+
 	private:
 		std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling;
 };

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();
-
-	std::shared_ptr<std::vector<double>> stateRewards = nullptr;
-	std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards = nullptr;
+	this->transitionSystem = tp.getMatrix();
+	
+	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/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/SparseStateRewardParser.h

@@ -20,7 +20,7 @@ class SparseStateRewardParser : Parser {
 		std::shared_ptr<std::vector<double>> getStateRewards() {
 			return this->stateRewards;
 		}
-	
+
 	private:
 		std::shared_ptr<std::vector<double>> stateRewards;
 };

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/SparseMatrix.h

@@ -25,10 +25,14 @@
 extern log4cplus::Logger logger;
 
 // Forward declaration for adapter classes.
-namespace storm { namespace adapters{ class GmmxxAdapter; class EigenAdapter; } }
+namespace storm { 
+	namespace adapters{ 
+		class GmmxxAdapter; 
+		class EigenAdapter; 
+	} 
+}
 
 namespace storm {
-
 namespace storage {
 
 /*!
@@ -50,7 +54,7 @@ public:
 	 * a row, we can simply iterate over the array (part) itself.
 	 */
 	typedef const uint_fast64_t * const constIndexIterator;
-	
+
 	/*!
 	 *	Iterator type if we want to iterate over elements.
 	 */
@@ -92,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
@@ -115,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());
 			}
 		}
 	}
@@ -209,7 +214,7 @@ public:
 
 		// Try to prepare the internal storage and throw an error in case of
 		// failure.
-		
+
 		// Get necessary pointers to the contents of the Eigen matrix.
 		const T* valuePtr = eigenSparseMatrix.valuePtr();
 		const _Index* indexPtr = eigenSparseMatrix.innerIndexPtr();
@@ -319,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) {
@@ -416,8 +420,8 @@ public:
 	/*!
 	 * Gets the matrix element at the given row and column to the given value.
 	 * NOTE: This function does not check the internal status for errors for performance reasons.
-	 * WARNING: It is possible to modify through this function. Usage only valid 
-	 * for elements EXISTING in the sparse matrix! If the requested value does not exist, 
+	 * WARNING: It is possible to modify through this function. Usage only valid
+	 * for elements EXISTING in the sparse matrix! If the requested value does not exist,
 	 * an exception will be thrown.
 	 * @param row The row in which the element is to be read.
 	 * @param col The column in which the element is to be read.
@@ -663,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;
 
@@ -888,6 +893,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.
@@ -922,7 +939,7 @@ public:
 	constIndexIterator endConstColumnIterator(uint_fast64_t row) const {
 		return &(this->columnIndications[0]) + this->rowIndications[row + 1];
 	}
-	
+
 	/*!
 	 *	Returns an iterator over the elements of the given row. The iterator
 	 *	will include no zero entries.
@@ -942,7 +959,7 @@ public:
 	constIterator endConstIterator(uint_fast64_t row) const {
 		return &(this->valueStorage[0]) + this->rowIndications[row + 1];
 	}
-	
+
 	/*!
 	 *	@brief Calculate sum of all entries in given row.
 	 *
@@ -959,13 +976,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:
@@ -1026,7 +1062,7 @@ private:
 		setState(MatrixStatus::Error);
 	}
 
-	/*! 
+	/*!
 	 * Sets the internal status to the given state if the current state is not
 	 * the error state.
 	 * @param new_state The new state to be switched to.

src/storm.cpp

@@ -99,18 +99,15 @@ 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")) {
 		storm::parser::PrctlParser parser(s->getString("test-prctl").c_str());
-		delete s;
 		return false;
 	}
 	
@@ -133,9 +130,7 @@ bool parseOptions(const int argc, const char* argv[]) {
  * Function to perform some cleanup.
  */
 void cleanUp() {
-	if (storm::settings::instance() != nullptr) {
-		delete storm::settings::instance();
-	}
+	// nothing here
 }
 
 void testCheckingDie(storm::models::Dtmc<double>& dtmc) {
@@ -221,12 +216,12 @@ 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, 4);
 	}
 	else std::cout << "Input is not DTMC" << std::endl;
-
-	// testCheckingDie(*dtmc);
-	// testCheckingCrowds(*dtmc);
-	// testCheckingSynchronousLeader(*dtmc, 4);
 }
 
 /*!

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
@@ -51,7 +53,7 @@ Settings::Settings(int const argc, char const * const argv[], char const * const
 	try {
 		// Initially fill description objects.
 		this->initDescriptions();
-		
+
 		// Take care of positional arguments.
 		Settings::positional.add("trafile", 1);
 		Settings::positional.add("labfile", 1);

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,19 +58,19 @@ 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;
 			}
-			
+
 			/*!
 			 *	@brief	Register a new module.
 			 *
@@ -118,18 +119,31 @@ namespace settings {
 				// Store module.
 				Settings::modules[ trigger ] = desc;
 			}
-	
+			
 			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, 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, 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,8 +188,35 @@ 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;
+				}
+			}
+	};
+	
 	/*!
 	 *	@brief	Print usage help.
 	 */

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/storm-tests.cpp

@@ -42,13 +42,11 @@ bool parseOptions(int const argc, char const * const 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;
     }