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

Former-commit-id: 62eaafecda

src/adapters/ExplicitModelAdapter.h

@@ -662,13 +662,13 @@ namespace storm {
                 bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC;
 
                 // Build the transition and reward matrices.
-                storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0);
-                storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder(0, 0, 0, !deterministicModel, 0);
+                storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
+                storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
                 modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder);
                 
                 // Finalize the resulting matrices.
                 modelComponents.transitionMatrix = transitionMatrixBuilder.build();
-                modelComponents.transitionRewardMatrix = transitionRewardMatrixBuilder.build(modelComponents.transitionMatrix.getRowCount());
+                modelComponents.transitionRewardMatrix = transitionRewardMatrixBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount());
                 
                 // Now build the state labeling.
                 modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation);

src/counterexamples/GenerateCounterexample.h

@@ -0,0 +1,146 @@
+
+#ifndef STORM_COUNTEREXAMPLES_GENERATECOUNTEREXAMPLE_H_
+#define STORM_COUNTEREXAMPLES_GENERATECOUNTEREXAMPLE_H_
+
+
+#include "src/models/Dtmc.h"
+#include "src/models/AtomicPropositionsLabeling.h"
+#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
+#include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
+#include "src/counterexamples/PathBasedSubsystemGenerator.h"
+#include "src/parser/PrctlParser.h"
+#include "src/properties/Prctl.h"
+#include "src/modelchecker/prctl/CreatePrctlModelChecker.h"
+
+
+#include "src/parser/PrctlFileParser.h"
+
+#include "src/exceptions/InvalidSettingsException.h"
+
+
+/*!
+ * Handles the counterexample generation control.
+ *
+ * @param parser An AutoParser to get the model from.
+ */
+ void generateCounterExample(std::shared_ptr<storm::models::AbstractModel<double>> model) {
+	LOG4CPLUS_INFO(logger, "Starting counterexample generation.");
+	LOG4CPLUS_INFO(logger, "Testing inputs...");
+
+	storm::settings::Settings* s  = storm::settings::Settings::getInstance();
+
+	// First test output directory.
+	std::string outPath = s->getOptionByLongName("counterExample").getArgument(0).getValueAsString();
+	if(outPath.back() != '/' && outPath.back() != '\\') {
+		LOG4CPLUS_ERROR(logger, "The output path is not valid.");
+		return;
+	}
+	std::ofstream testFile(outPath + "test.dot");
+	if(testFile.fail()) {
+		LOG4CPLUS_ERROR(logger, "The output path is not valid.");
+		return;
+	}
+	testFile.close();
+	std::remove((outPath + "test.dot").c_str());
+
+ 	// Differentiate between model types.
+	if(model->getType() != storm::models::DTMC) {
+		LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported.");
+		return;
+	}
+
+	// Get the Dtmc back from the AbstractModel
+	// Note that the ownership of the object referenced by dtmc lies at the main function.
+	// Thus, it must not be deleted.
+	storm::models::Dtmc<double> dtmc = *(model->as<storm::models::Dtmc<double>>());
+	LOG4CPLUS_INFO(logger, "Model is a DTMC.");
+
+	// Get specified PRCTL formulas.
+	if(!s->isSet("prctl")) {
+		LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified.");
+		return;
+	}
+
+	std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString();
+	LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << ".");
+	std::list<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile);
+
+	// Test for each formula if a counterexample can be generated for it.
+	if(formulaList.size() == 0) {
+		LOG4CPLUS_ERROR(logger, "No PRCTL formula found.");
+		return;
+	}
+
+	// Get prctl file name without the filetype
+	uint_fast64_t first = 0;
+	if(chosenPrctlFile.find('/') != std::string::npos) {
+		first = chosenPrctlFile.find_last_of('/') + 1;
+	} else if(chosenPrctlFile.find('\\') != std::string::npos) {
+		first = chosenPrctlFile.find_last_of('\\') + 1;
+	}
+
+	uint_fast64_t length;
+	if(chosenPrctlFile.find_last_of('.') != std::string::npos && chosenPrctlFile.find_last_of('.') >= first) {
+		length = chosenPrctlFile.find_last_of('.') - first;
+	} else {
+		length = chosenPrctlFile.length() - first;
+	}
+
+	std::string outFileName = chosenPrctlFile.substr(first, length);
+
+	// Test formulas and do generation
+	uint_fast64_t fIndex = 0;
+	for (auto formula : formulaList) {
+
+		// First check if it is a formula type for which a counterexample can be generated.
+		if (std::dynamic_pointer_cast<storm::properties::prctl::AbstractStateFormula<double>>(formula->getChild()).get() == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula.");
+			continue;
+		}
+
+		std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>> stateForm = std::static_pointer_cast<storm::properties::prctl::AbstractStateFormula<double>>(formula->getChild());
+
+		// Do some output
+		std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl;
+		LOG4CPLUS_INFO(logger, "Generating counterexample for formula " + std::to_string(fIndex) + ": ");
+		std::cout << "\t" << formula->toString() << "\n" << std::endl;
+		LOG4CPLUS_INFO(logger, formula->toString());
+
+		// Now check if the model does not satisfy the formula.
+		// That is if there is at least one initial state of the model that does not.
+
+		// Also raise the logger threshold for the log file, so that the model check infos aren't logged (useless and there are lots of them)
+		// Lower it again after the model check.
+		logger.getAppender("mainFileAppender")->setThreshold(log4cplus::WARN_LOG_LEVEL);
+		storm::storage::BitVector result = stateForm->check(*createPrctlModelChecker(dtmc));
+		logger.getAppender("mainFileAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
+
+		if((result & dtmc.getInitialStates()).getNumberOfSetBits() == dtmc.getInitialStates().getNumberOfSetBits()) {
+			std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl;
+			LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample.");
+			continue;
+		}
+
+		// Generate counterexample
+		storm::models::Dtmc<double> counterExample = storm::counterexamples::PathBasedSubsystemGenerator<double>::computeCriticalSubsystem(dtmc, stateForm);
+
+		LOG4CPLUS_INFO(logger, "Found counterexample.");
+
+		// Output counterexample
+		// Do standard output
+		std::cout << "Found counterexample with following properties: " << std::endl;
+		counterExample.printModelInformationToStream(std::cout);
+		std::cout << "For full Dtmc see " << outFileName << "_" << fIndex << ".dot at given output path.\n\n" << std::endl;
+
+		// Write the .dot file
+		std::ofstream outFile(outPath + outFileName + "_" + std::to_string(fIndex) + ".dot");
+		if(outFile.good()) {
+			counterExample.writeDotToStream(outFile, true, nullptr, nullptr, nullptr, nullptr, nullptr, nullptr, true);
+			outFile.close();
+		}
+
+		fIndex++;
+	}
+ }
+ 
+#endif

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@@ -347,7 +347,7 @@ namespace storm {
 
                     // Finally, we are ready to create the SSP matrix and right-hand side of the SSP.
                     std::vector<ValueType> b;
-                    typename storm::storage::SparseMatrixBuilder<ValueType> sspMatrixBuilder(0, 0, 0, true, numberOfStatesNotInMecs + mecDecomposition.size());
+                    typename storm::storage::SparseMatrixBuilder<ValueType> sspMatrixBuilder(0, 0, 0, false, true, numberOfStatesNotInMecs + mecDecomposition.size());
                     
                     // If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications).
                     uint_fast64_t currentChoice = 0;

src/modelchecker/prctl/CreatePrctlModelChecker.h

@@ -0,0 +1,43 @@
+#ifndef STORM_MODELCHECKER_PRCTL_CREATEPRCTLMODELCHECKER_H_
+#define STORM_MODELCHECKER_PRCTL_CREATEPRCTLMODELCHECKER_H_
+
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "src/solver/GmmxxLinearEquationSolver.h"
+#include "src/solver/NativeLinearEquationSolver.h"
+#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
+#include "src/solver/GurobiLpSolver.h"
+/*!
+ * Creates a model checker for the given DTMC that complies with the given options.
+ *
+ * @param dtmc A reference to the DTMC for which the model checker is to be created.
+ * @return A pointer to the resulting model checker.
+ */
+storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Dtmc<double> const & dtmc) {
+    // Create the appropriate model checker.
+	storm::settings::Settings* s = storm::settings::Settings::getInstance();
+	std::string const& linsolver = s->getOptionByLongName("linsolver").getArgument(0).getValueAsString();
+	if (linsolver == "gmm++") {
+		return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
+	} else if (linsolver == "native") {
+		return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc, new storm::solver::NativeLinearEquationSolver<double>());
+    }
+    
+	// The control flow should never reach this point, as there is a default setting for matrixlib.
+	std::string message = "No matrix library suitable for DTMC model checking has been set.";
+	throw storm::exceptions::InvalidSettingsException() << message;
+	return nullptr;
+}
+
+/*!
+ * Creates a model checker for the given MDP that complies with the given options.
+ *
+ * @param mdp The Dtmc that the model checker will check
+ * @return
+ */
+storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Mdp<double> const & mdp) {
+    // Create the appropriate model checker.
+    return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp);
+}
+
+#endif

src/models/AbstractModel.h

@@ -309,7 +309,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		 * @return True if this model has a state reward model.
 		 */
 		bool hasStateRewards() const {
-			return stateRewardVector;
+			return static_cast<bool>(stateRewardVector);
 		}
 
 		/*!
@@ -317,7 +317,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		 * @return True if this model has a transition reward model.
 		 */
 		bool hasTransitionRewards() const {
-			return transitionRewardMatrix;
+			return static_cast<bool>(transitionRewardMatrix);
 		}
     
         /*!
@@ -325,7 +325,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
          * @return True if this model has a labeling.
          */
         bool hasChoiceLabeling() const {
-            return choiceLabeling;
+            return static_cast<bool>(choiceLabeling);
         }
 
 		/*!

src/models/MarkovAutomaton.h

@@ -126,7 +126,7 @@ namespace storm {
                     //uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates;
                     
                     // Create the matrix for the new transition relation and the corresponding nondeterministic choice vector.
-                    storm::storage::SparseMatrixBuilder<T> newTransitionMatrixBuilder(0, 0, 0, true, this->getNumberOfStates());
+                    storm::storage::SparseMatrixBuilder<T> newTransitionMatrixBuilder(0, 0, 0, false, true, this->getNumberOfStates());
                     
                     // Now copy over all choices that need to be kept.
                     uint_fast64_t currentChoice = 0;

src/models/Mdp.h

@@ -139,7 +139,7 @@ public:
         
         std::vector<boost::container::flat_set<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling();
         
-        storm::storage::SparseMatrixBuilder<T> transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true);
+        storm::storage::SparseMatrixBuilder<T> transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true, true);
         std::vector<boost::container::flat_set<uint_fast64_t>> newChoiceLabeling;
         
         // Check for each choice of each state, whether the choice labels are fully contained in the given label set.

src/parser/AtomicPropositionLabelingParser.cpp

@@ -34,7 +34,7 @@ namespace storm {
 			}
 
 			MappedFile file(filename.c_str());
-			char* buf = file.getData();
+			char const* buf = file.getData();
 
 			// First pass: Count the number of propositions.
 			bool foundDecl = false, foundEnd = false;

src/parser/AutoParser.cpp

@@ -12,6 +12,7 @@
 #include "src/parser/DeterministicModelParser.h"
 #include "src/parser/NondeterministicModelParser.h"
 #include "src/parser/MarkovAutomatonParser.h"
+#include "src/exceptions/ExceptionMacros.h"
 #include "src/exceptions/WrongFormatException.h"
 
 #include "src/utility/cstring.h"
@@ -74,25 +75,30 @@ namespace storm {
 
 			// Open the file.
 			MappedFile file(filename.c_str());
-			char* buf = file.getData();
+            
+			LOG_THROW(file.getDataSize() >= STORM_PARSER_AUTOPARSER_HINT_LENGTH, storm::exceptions::WrongFormatException, "File too short to be readable.");
+			char const* fileData = file.getData();
+            
+			char filehintBuffer[STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1];
+			memcpy(filehintBuffer, fileData, STORM_PARSER_AUTOPARSER_HINT_LENGTH);
+			filehintBuffer[STORM_PARSER_AUTOPARSER_HINT_LENGTH] = 0;
 
 			// Find and read in the hint.
-			char hint[65];
-			// %60s => The input hint can be AT MOST 60 chars long.
+			std::string formatString = "%" + std::to_string(STORM_PARSER_AUTOPARSER_HINT_LENGTH) + "s";
+			char hint[5];
 		#ifdef WINDOWS
-			sscanf_s(buf, "%60s", hint, sizeof(hint));
+			sscanf_s(filehintBuffer, formatString.c_str(), hint, STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1);
 		#else
-			sscanf(buf, "%60s", hint);
+			int ret = sscanf(filehintBuffer, formatString.c_str(), hint);
 		#endif
-
 			for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
-
+            
 			// Check if the hint value is known and store the appropriate enum value.
-			if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC;
-			else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC;
-			else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP;
-			else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP;
-			else if (strncmp(hint, "MA", sizeof(hint)) == 0) hintType = storm::models::MA;
+			if (strcmp(hint, "DTMC") == 0) hintType = storm::models::DTMC;
+			else if (strcmp(hint, "CTMC") == 0) hintType = storm::models::CTMC;
+			else if (strcmp(hint, "MDP") == 0) hintType = storm::models::MDP;
+			else if (strcmp(hint, "CTMDP") == 0) hintType = storm::models::CTMDP;
+			else if (strcmp(hint, "MA") == 0) hintType = storm::models::MA;
 
 			return hintType;
 		}

src/parser/AutoParser.h

@@ -5,6 +5,8 @@
 
 #include <string>
 
+#define STORM_PARSER_AUTOPARSER_HINT_LENGTH (10ull)
+
 namespace storm {
 
 	/*!
@@ -47,6 +49,8 @@ namespace storm {
                                                                                     std::string const & transitionRewardFilename = "");
 
 		private:
+            // Define the maximal length of a hint in the file.
+            static uint_fast64_t hintLength;
 
 			/*!
 			 *	Opens the given file and parses the file format hint.

src/parser/DeterministicSparseTransitionParser.cpp

@@ -53,7 +53,7 @@ namespace storm {
 
 				// Open file.
 				MappedFile file(filename.c_str());
-				char* buf = file.getData();
+				char const* buf = file.getData();
 
 				// Perform first pass, i.e. count entries that are not zero.
 				bool insertDiagonalEntriesIfMissing = !isRewardFile;
@@ -115,6 +115,23 @@ namespace storm {
 						buf = trimWhitespaces(buf);
 					}
 				} else {
+                    // Read first row and add self-loops if necessary.
+                    char const* tmp;
+                    row = checked_strtol(buf, &tmp);
+                    
+                    if (row > 0) {
+                        for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) {
+                            hadDeadlocks = true;
+                            if (fixDeadlocks) {
+                                resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne<double>());
+                                LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
+                            } else {
+                                LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
+                                // Before throwing the appropriate exception we will give notice of all deadlock states.
+                            }
+                        }
+                    }
+                    
 					while (buf[0] != '\0') {
 
 						// Read next transition.
@@ -139,7 +156,6 @@ namespace storm {
 								hadDeadlocks = true;
 								if (fixDeadlocks) {
 									resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne<double>());
-									rowHadDiagonalEntry = true;
 									LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
 								} else {
 									LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
@@ -193,7 +209,7 @@ namespace storm {
 				return result;
 		}
 
-		DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, bool insertDiagonalEntriesIfMissing) {
+		DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char const* buf, bool insertDiagonalEntriesIfMissing) {
 
 			DeterministicSparseTransitionParser::FirstPassResult result;
 
@@ -207,6 +223,16 @@ namespace storm {
 			 // Check all transitions for non-zero diagonal entries and deadlock states.
 			uint_fast64_t row, col, lastRow = 0, lastCol = -1;
 			bool rowHadDiagonalEntry = false;
+            
+            // Read first row and reserve space for self-loops if necessary.
+            char const* tmp;
+            row = checked_strtol(buf, &tmp);
+            if (row > 0) {
+                for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) {
+                    ++result.numberOfNonzeroEntries;
+                }
+            }
+            
 			while (buf[0] != '\0') {
 
 				// Read the transition.

src/parser/DeterministicSparseTransitionParser.h

@@ -67,7 +67,7 @@ namespace storm {
 			 * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
 			 * @return A structure representing the result of the first pass.
 			 */
-			static FirstPassResult firstPass(char* buffer, bool insertDiagonalEntriesIfMissing = true);
+			static FirstPassResult firstPass(char const* buffer, bool insertDiagonalEntriesIfMissing = true);
 
 			/*
 			 * The main parsing routine.

src/parser/MappedFile.cpp

@@ -42,15 +42,15 @@ namespace storm {
 				LOG4CPLUS_ERROR(logger, "Error in open(" << filename << "): Probably, we may not read this file.");
 				throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file.";
 			}
-
-			this->data = reinterpret_cast<char*>(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0));
-			if (this->data == reinterpret_cast<char*>(-1)) {
+            
+			this->data = static_cast<char*>(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0));
+			if (this->data == MAP_FAILED) {
 				close(this->file);
 				LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << "): " << std::strerror(errno));
 				throw exceptions::FileIoException() << "MappedFile Error in mmap(): " << std::strerror(errno);
 			}
 			this->dataEnd = this->data + this->st.st_size;
-		#elif defined WINDOWS
+        #elif defined WINDOWS
 
 			// Do file mapping for windows.
 			// _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile()
@@ -100,13 +100,17 @@ namespace storm {
 			return fin.good();
 		}
 
-		char* MappedFile::getData() {
+		char const* MappedFile::getData() const {
 			return data;
 		}
 
-		char* MappedFile::getDataEnd() {
+		char const* MappedFile::getDataEnd() const {
 			return dataEnd;
 		}
+            
+        std::size_t MappedFile::getDataSize() const {
+            return this->getDataEnd() - this->getData();
+        }
 
 	} // namespace parser
 } // namespace storm

src/parser/MappedFile.h

@@ -8,6 +8,7 @@
 #ifndef STORM_PARSER_MAPPEDFILE_H_
 #define STORM_PARSER_MAPPEDFILE_H_
 
+#include <cstddef>
 #include <sys/stat.h>
 
 #include "src/utility/OsDetection.h"
@@ -61,15 +62,20 @@ namespace storm {
 			 *
 			 * @return A pointer to the first character of the mapped file data.
 			 */
-			char* getData();
+			char const* getData() const;
 
 			/*!
 			 * Returns a pointer to the end of the mapped file data.
 			 *
 			 * @return A pointer to the first position after the last character of the mapped file data.
 			 */
-			char* getDataEnd();
+			char const* getDataEnd() const;
 
+            /*!
+             * Returns the size of the mapped file data.
+             */
+            std::size_t getDataSize() const;
+            
 		private:
 
 			//! A pointer to the mapped file content.

src/parser/MarkovAutomatonSparseTransitionParser.cpp

@@ -12,7 +12,7 @@ namespace storm {
 
 		using namespace storm::utility::cstring;
 
-		MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf) {
+		MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char const* buf) {
 			MarkovAutomatonSparseTransitionParser::FirstPassResult result;
 
 			bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
@@ -154,7 +154,7 @@ namespace storm {
 			return result;
 		}
 
-		MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char* buf, FirstPassResult const& firstPassResult) {
+		MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char const* buf, FirstPassResult const& firstPassResult) {
 			Result result(firstPassResult);
 
 			bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
@@ -271,7 +271,7 @@ namespace storm {
 
 			// Open file and prepare pointer to buffer.
 			MappedFile file(filename.c_str());
-			char* buf = file.getData();
+			char const* buf = file.getData();
 
 			return secondPass(buf, firstPass(buf));
 		}

src/parser/MarkovAutomatonSparseTransitionParser.h

@@ -85,7 +85,7 @@ namespace storm {
 			 * @param buffer The buffer that cointains the input.
 			 * @return A structure representing the result of the first pass.
 			 */
-			static FirstPassResult firstPass(char* buffer);
+			static FirstPassResult firstPass(char const* buffer);
 
 			/*!
 			 * Performs the second pass on the input pointed to by the given buffer with the information of the first pass.
@@ -94,7 +94,7 @@ namespace storm {
 			 * @param firstPassResult The result of the first pass performed on the same input.
 			 * @return A structure representing the result of the second pass.
 			 */
-			static Result secondPass(char* buffer, FirstPassResult const& firstPassResult);
+			static Result secondPass(char const* buffer, FirstPassResult const& firstPassResult);
 		};
 
 	} // namespace parser

src/parser/NondeterministicSparseTransitionParser.cpp

@@ -50,7 +50,7 @@ namespace storm {
 
 			// Open file.
 			MappedFile file(filename.c_str());
-			char* buf = file.getData();
+			char const* buf = file.getData();
 
 			// Perform first pass, i.e. obtain number of columns, rows and non-zero elements.
 			NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.getData(), isRewardFile, modelInformation);
@@ -92,9 +92,9 @@ namespace storm {
 			LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << firstPass.choices << " x " << (firstPass.highestStateIndex+1) << " with " << firstPass.numberOfNonzeroEntries << " entries.");
 			storm::storage::SparseMatrixBuilder<double> matrixBuilder;
 			if(!isRewardFile) {
-				matrixBuilder = storm::storage::SparseMatrixBuilder<double>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, firstPass.highestStateIndex + 1);
+				matrixBuilder = storm::storage::SparseMatrixBuilder<double>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, true, firstPass.highestStateIndex + 1);
 			} else {
-				matrixBuilder = storm::storage::SparseMatrixBuilder<double>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, modelInformation.getRowGroupCount());
+				matrixBuilder = storm::storage::SparseMatrixBuilder<double>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, true, modelInformation.getRowGroupCount());
 			}
 
 			// Initialize variables for the parsing run.
@@ -179,7 +179,7 @@ namespace storm {
 			// Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices.
 			if(isRewardFile) {
 				// We already have rowGroup 0.
-				for(uint_fast64_t index = 1; index < modelInformation.getRowGroupIndices().size(); index++) {
+				for(uint_fast64_t index = 1; index < modelInformation.getRowGroupIndices().size() - 1; index++) {
 					matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[index]);
 				}
 			} else {
@@ -200,7 +200,7 @@ namespace storm {
 			return resultMatrix;
 		}
 
-		NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, bool isRewardFile, storm::storage::SparseMatrix<double> const & modelInformation) {
+		NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char const* buf, bool isRewardFile, storm::storage::SparseMatrix<double> const & modelInformation) {
 
 			// Check file header and extract number of transitions.
 

src/parser/NondeterministicSparseTransitionParser.h

@@ -74,7 +74,7 @@ namespace storm {
 			 * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
 			 * @return A structure representing the result of the first pass.
 			 */
-			static FirstPassResult firstPass(char* buffer, bool isRewardFile, storm::storage::SparseMatrix<double> const & modelInformation);
+			static FirstPassResult firstPass(char const* buffer, bool isRewardFile, storm::storage::SparseMatrix<double> const & modelInformation);
 
 			/*!
 			 * The main parsing routine.

src/parser/SparseStateRewardParser.cpp

@@ -29,7 +29,7 @@ namespace storm {
 			}
 
 			MappedFile file(filename.c_str());
-			char* buf = file.getData();
+			char const* buf = file.getData();
 
 			// Create state reward vector with given state count.
 			std::vector<double> stateRewards(stateCount);

src/storage/SparseMatrix.cpp

@@ -9,6 +9,7 @@
 
 #include "src/storage/SparseMatrix.h"
 #include "src/exceptions/InvalidStateException.h"
+#include "src/exceptions/ExceptionMacros.h"
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
@@ -53,37 +54,27 @@ namespace storm {
         }
         
         template<typename ValueType>
-        SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool hasCustomRowGrouping, index_type rowGroups) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), hasCustomRowGrouping(hasCustomRowGrouping), rowGroupCountSet(rowGroups != 0), rowGroupCount(rowGroups), rowGroupIndices(), storagePreallocated(rows != 0 && columns != 0 && entries != 0), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), currentRowGroup(0) {
-            this->prepareInternalStorage();
+        SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroup(0) {
+            // Prepare the internal storage.
+            if (initialRowCountSet) {
+                rowIndications.reserve(initialRowCount + 1);
+            }
+            if (initialEntryCountSet) {
+                columnsAndValues.reserve(initialEntryCount);
+            }
+            if (initialRowGroupCountSet) {
+                rowGroupIndices.reserve(initialRowGroupCount + 1);
+            }
+            rowIndications.push_back(0);
         }
         
         template<typename ValueType>
         void SparseMatrixBuilder<ValueType>::addNextValue(index_type row, index_type column, ValueType const& value) {
-            // Depending on whether the internal data storage was preallocated or not, adding the value is done somewhat
-            // differently.
-            if (storagePreallocated) {
-                // Check whether the given row and column positions are valid and throw error otherwise.
-                if (row >= rowCount || column >= columnCount) {
-                    throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding entry at out-of-bounds position (" << row << ", " << column << ") in matrix of size (" << rowCount << ", " << columnCount << ").";
-                }
-            } else {
-                if (rowCountSet) {
-                    if (row >= rowCount) {
-                        throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding entry at out-of-bounds row " << row << " in matrix with " << rowCount << " rows.";
-                    }
-                }
-                if (columnCountSet) {
-                    if (column >= columnCount) {
-                        throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding entry at out-of-bounds column " << column << " in matrix with " << columnCount << " columns.";
-                    }
-                }
-            }
-            
             // Check that we did not move backwards wrt. the row.
             if (row < lastRow) {
                 throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding an element in row " << row << ", but an element in row " << lastRow << " has already been added.";
             }
-            
+
             // Check that we did not move backwards wrt. to column.
             if (row == lastRow && column < lastColumn) {
                 throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding an element in column " << column << " in row " << row << ", but an element in column " << lastColumn << " has already been added in that row.";
@@ -91,24 +82,9 @@ namespace storm {
             
             // If we switched to another row, we have to adjust the missing entries in the row indices vector.
             if (row != lastRow) {
-                if (storagePreallocated) {
-                    // If the storage was preallocated, we can access the elements in the vectors with the subscript
-                    // operator.
-                    for (index_type i = lastRow + 1; i <= row; ++i) {
-                        rowIndications[i] = currentEntryCount;
-                    }
-                } else {
-                    // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations.
-                    for (index_type i = lastRow + 1; i <= row; ++i) {
-                        rowIndications.push_back(currentEntryCount);
-                    }
-                }
-                
-                if (!hasCustomRowGrouping) {
-                    for (index_type i = lastRow + 1; i <= row; ++i) {
-                        rowGroupIndices.push_back(i);
-                        ++currentRowGroup;
-                    }
+                // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations.
+                for (index_type i = lastRow + 1; i <= row; ++i) {
+                    rowIndications.push_back(currentEntryCount);
                 }
                 
                 lastRow = row;
@@ -117,109 +93,76 @@ namespace storm {
             lastColumn = column;
             
             // Finally, set the element and increase the current size.
-            if (storagePreallocated) {
-                columnsAndValues[currentEntryCount] = std::make_pair(column, value);
-            } else {
-                columnsAndValues.emplace_back(column, value);
-                if (!columnCountSet) {
-                    columnCount = std::max(columnCount, column + 1);
-                }
-                if (!rowCountSet) {
-                    rowCount = row + 1;
-                }
-            }
+            columnsAndValues.emplace_back(column, value);
+            highestColumn = std::max(highestColumn, column);
             ++currentEntryCount;
+
+            // In case we did not expect this value, we throw an exception.
+            if (forceInitialDimensions) {
+                LOG_THROW(!initialRowCountSet || lastRow < initialRowCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal row " << lastRow << ".");
+                LOG_THROW(!initialColumnCountSet || lastColumn < initialColumnCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal column " << lastColumn << ".");
+                LOG_THROW(!initialEntryCountSet || currentEntryCount <= initialEntryCount, storm::exceptions::OutOfRangeException, "Too many entries in matrix, expected only " << initialEntryCount << ".");
+            }
         }
         
         template<typename ValueType>
         void SparseMatrixBuilder<ValueType>::newRowGroup(index_type startingRow) {
-            if (!hasCustomRowGrouping) {
-                throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: matrix was not created to have a custom row grouping.";
-            } else if (rowGroupIndices.size() > 0 && startingRow < rowGroupIndices.back()) {
-                throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: illegal row group with negative size.";
-            }
-            if (rowGroupCountSet) {
-                rowGroupIndices[currentRowGroup] = startingRow;
-                ++currentRowGroup;
-            } else {
-                rowGroupIndices.push_back(startingRow);
-            }
+            LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping.");
+            LOG_THROW(rowGroupIndices.empty() || startingRow >= rowGroupIndices.back(), storm::exceptions::InvalidStateException, "Illegal row group with negative size.");
+            rowGroupIndices.push_back(startingRow);
+            ++currentRowGroup;
         }
         
         template<typename ValueType>
         SparseMatrix<ValueType> SparseMatrixBuilder<ValueType>::build(index_type overriddenRowCount, index_type overriddenColumnCount, index_type overriddenRowGroupCount) {
-            // Check whether it's safe to finalize the matrix and throw error otherwise.
-            if (storagePreallocated && currentEntryCount != entryCount) {
-                throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::build: expected " << entryCount << " entries, but got " << currentEntryCount << " instead.";
-            } else {
-                // Fill in the missing entries in the row indices array, as there may be empty rows at the end.
-                if (storagePreallocated) {
-                    for (index_type i = lastRow + 1; i < rowCount; ++i) {
-                        rowIndications[i] = currentEntryCount;
-                    }
-                } else {
-                    if (!rowCountSet) {
-                        rowCount = std::max(overriddenRowCount, rowCount);
-                    }
-                    for (index_type i = lastRow + 1; i < rowCount; ++i) {
-                        rowIndications.push_back(currentEntryCount);
-                    }
-                }
-                
-                // We put a sentinel element at the last position of the row indices array. This eases iteration work,
-                // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for
-                // the first and last row.
-                if (storagePreallocated) {
-                    rowIndications[rowCount] = currentEntryCount;
-                } else {
-                    rowIndications.push_back(currentEntryCount);
-                    if (!columnCountSet) {
-                        columnCount = std::max(columnCount, overriddenColumnCount);
-                    }
-                }
-                
-                entryCount = currentEntryCount;
-                
-                if (hasCustomRowGrouping && rowGroupCountSet) {
-                    rowGroupIndices[rowGroupCount] = rowCount;
-                } else {
-                    if (!hasCustomRowGrouping) {
-                        for (index_type i = currentRowGroup; i < rowCount; ++i) {
-                            rowGroupIndices.push_back(i + 1);
-                        }
-                    } else {
-                        overriddenRowGroupCount = std::max(overriddenRowGroupCount, currentRowGroup + 1);
-                        for (index_type i = currentRowGroup; i < overriddenRowGroupCount; ++i) {
-                            rowGroupIndices.push_back(rowCount);
-                        }
-                    }
-                }
+            uint_fast64_t rowCount = lastRow + 1;
+            if (initialRowCountSet && forceInitialDimensions) {
+                LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << ".");
+                rowCount = std::max(rowCount, initialRowCount);
             }
+            rowCount = std::max(rowCount, overriddenRowCount);
             
-            return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
-        }
-        
-        template<typename ValueType>
-        void SparseMatrixBuilder<ValueType>::prepareInternalStorage() {
-            // Only allocate the memory for the matrix contents if the dimensions of the matrix are already known.
-            if (storagePreallocated) {
-                columnsAndValues = std::vector<MatrixEntry<index_type, ValueType>>(entryCount, MatrixEntry<index_type, ValueType>(0, storm::utility::constantZero<ValueType>()));
-                rowIndications = std::vector<index_type>(rowCount + 1, 0);
-            } else {
-                rowIndications.push_back(0);
+            // If the current row count was overridden, we may need to add empty rows.
+            for (index_type i = lastRow + 1; i < rowCount; ++i) {
+                rowIndications.push_back(currentEntryCount);
             }
             
-            // Only allocate the memory for the row grouping of the matrix contents if the number of groups is already
-            // known.
-            if (hasCustomRowGrouping && rowGroupCountSet) {
-                rowGroupIndices = std::vector<index_type>(rowGroupCount + 1, 0);
+            // We put a sentinel element at the last position of the row indices array. This eases iteration work,
+            // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for
+            // the first and last row.
+            rowIndications.push_back(currentEntryCount);
+
+            uint_fast64_t columnCount = highestColumn + 1;
+            if (initialColumnCountSet && forceInitialDimensions) {
+                LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << ".");
+                columnCount = std::max(columnCount, initialColumnCount);
+            }
+            columnCount = std::max(columnCount, overriddenColumnCount);
+
+            uint_fast64_t entryCount = currentEntryCount;
+            if (initialEntryCountSet && forceInitialDimensions) {
+                LOG_THROW(entryCount == initialEntryCount, storm::exceptions::InvalidStateException, "Expected " << initialEntryCount << " entries, but got " << entryCount << ".");
+            }
+            
+            // Check whether row groups are missing some entries.
+            if (!hasCustomRowGrouping) {
+                for (index_type i = 0; i <= rowCount; ++i) {
+                    rowGroupIndices.push_back(i);
+                }
             } else {
-                if (hasCustomRowGrouping) {
-                    // Nothing to do in this case
-                } else {
-                    rowGroupIndices.push_back(0);
+                uint_fast64_t rowGroupCount = currentRowGroup;
+                if (initialRowGroupCountSet && forceInitialDimensions) {
+                    LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << ".");
+                    rowGroupCount = std::max(rowGroupCount, initialRowGroupCount);
+                }
+                rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount);
+
+                for (index_type i = currentRowGroup; i <= rowGroupCount; ++i) {
+                    rowGroupIndices.push_back(rowCount);
                 }
             }
+
+            return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
         }
         
         template<typename ValueType>
@@ -531,7 +474,7 @@ namespace storm {
             }
             
             // Create and initialize resulting matrix.
-            SparseMatrixBuilder<ValueType> matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true);
+            SparseMatrixBuilder<ValueType> matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true, true);
             
             // Create a temporary vector that stores for each index whose bit is set to true the number of bits that
             // were set before that particular index.
@@ -806,7 +749,7 @@ namespace storm {
         void SparseMatrix<ValueType>::multiplyWithVectorSequential(std::vector<ValueType> const& vector, std::vector<ValueType>& result) const {
             const_iterator it = this->begin();
             const_iterator ite;
-            typename std::vector<index_type>::const_iterator rowIterator = rowIndications.begin();
+            std::vector<index_type>::const_iterator rowIterator = rowIndications.begin();
             typename std::vector<ValueType>::iterator resultIterator = result.begin();
             typename std::vector<ValueType>::iterator resultIteratorEnd = result.end();
             

src/storage/SparseMatrix.h

@@ -122,16 +122,20 @@ namespace storm {
             
             /*!
              * Constructs a sparse matrix builder producing a matrix with the given number of rows, columns and entries.
+             * The number of rows, columns and entries is reserved upon creation. If more rows/columns or entries are
+             * added, this will possibly lead to a reallocation.
              *
              * @param rows The number of rows of the resulting matrix.
              * @param columns The number of columns of the resulting matrix.
              * @param entries The number of entries of the resulting matrix.
+             * @param forceDimensions If this flag is set, the matrix is expected to have exactly the given number of
+             * rows, columns and entries for all of these entities that are set to a nonzero value.
              * @param hasCustomRowGrouping A flag indicating whether the builder is used to create a non-canonical
              * grouping of rows for this matrix.
              * @param rowGroups The number of row groups of the resulting matrix. This is only relevant if the matrix
              * has a custom row grouping.
              */
-            SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool hasCustomRowGrouping = false, index_type rowGroups = 0);
+            SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool forceDimensions = true, bool hasCustomRowGrouping = false, index_type rowGroups = 0);
             
             /*!
              * Sets the matrix entry at the given row and column to the given value. After all entries have been added,
@@ -178,42 +182,38 @@ namespace storm {
             SparseMatrix<value_type> build(index_type overriddenRowCount = 0, index_type overriddenColumnCount = 0, index_type overriddenRowGroupCount = 0);
             
         private:
-            /*!
-             * Prepares the internal storage of the builder. This relies on the number of entries and the number of rows
-             * being set correctly. They may, however, be zero, in which case the insertion of elements in the builder
-             * will cause occasional reallocations.
-             */
-            void prepareInternalStorage();
-
-            // A flag indicating whether the number of rows was set upon construction.
-            bool rowCountSet;
+            // A flag indicating whether a row count was set upon construction.
+            bool initialRowCountSet;
             
-            // The number of rows of the matrix.
-            index_type rowCount;
+            // The row count that was initially set (if any).
+            index_type initialRowCount;
             
-            // A flag indicating whether the number of columns was set upon construction.
-            bool columnCountSet;
+            // A flag indicating whether a column count was set upon construction.
+            bool initialColumnCountSet;
+
+            // The column count that was initially set (if any).
+            index_type initialColumnCount;
             
-            // The number of columns of the matrix.
-            index_type columnCount;
+            // A flag indicating whether an entry count was set upon construction.
+            bool initialEntryCountSet;
             
             // The number of entries in the matrix.
-            index_type entryCount;
+            index_type initialEntryCount;
+            
+            // A flag indicating whether the initially given dimensions are to be enforced on the resulting matrix.
+            bool forceInitialDimensions;
             
             // A flag indicating whether the builder is to construct a custom row grouping for the matrix.
             bool hasCustomRowGrouping;
             
             // A flag indicating whether the number of row groups was set upon construction.
-            bool rowGroupCountSet;
+            bool initialRowGroupCountSet;
             
             // The number of row groups in the matrix.
-            index_type rowGroupCount;
+            index_type initialRowGroupCount;
             
             std::vector<index_type> rowGroupIndices;
             
-            // Stores whether the storage of the matrix was preallocated or not.
-            bool storagePreallocated;
-            
             // The storage for the columns and values of all entries in the matrix.
             std::vector<MatrixEntry<index_type, value_type>> columnsAndValues;
             
@@ -235,6 +235,9 @@ namespace storm {
             // entry into a matrix.
             index_type lastColumn;
             
+            // Stores the highest column at which an entry was inserted into the matrix.
+            index_type highestColumn;
+            
             // Stores the currently active row group. This is used for correctly constructing the row grouping of the
             // matrix.
             index_type currentRowGroup;

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -161,7 +161,7 @@ namespace storm {
                 
                 bool recursionStepIn = false;
                 for (; successorIt != model.getRows(currentState).end(); ++successorIt) {
-                    if (subsystem.get(successorIt->getColumn())) {
+                    if (subsystem.get(successorIt->getColumn()) && successorIt->getValue() != storm::utility::constantZero<ValueType>()) {
                         if (currentState == successorIt->getColumn()) {
                             statesWithSelfLoop.set(currentState);
                         }

src/storm.cpp

@@ -13,14 +13,18 @@
  *  Description: Central part of the application containing the main() Method
  */
 
-#include "src/utility/OsDetection.h"
-#include <iostream>
+#include "src/utility/Initialize.h"
 #include <fstream>
 #include <cstdio>
 #include <climits>
 #include <sstream>
 #include <vector>
 #include <chrono>
+#include <iostream>
+#include <iomanip>
+
+
+
 
 #include "storm-config.h"
 #include "storm-version.h"
@@ -30,12 +34,14 @@
 #include "src/storage/MaximalEndComponentDecomposition.h"
 #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
 #include "src/models/AtomicPropositionsLabeling.h"
+#include "src/modelchecker/prctl/CreatePrctlModelChecker.h"
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 #include "src/solver/GmmxxLinearEquationSolver.h"
 #include "src/solver/NativeLinearEquationSolver.h"
 #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
 #include "src/solver/GurobiLpSolver.h"
+#include "src/counterexamples/GenerateCounterexample.h"
 #include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
 #include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
 #include "src/counterexamples/PathBasedSubsystemGenerator.h"
@@ -45,251 +51,20 @@
 #include "src/utility/ErrorHandling.h"
 #include "src/properties/Prctl.h"
 #include "src/utility/vector.h"
-#include "src/utility/OsDetection.h"
+#include "src/utility/CLI.h"
 
-#include "src/settings/Settings.h"
-// Registers all standard options
-#include "src/utility/StormOptions.h" 
 
 #include "src/parser/PrctlFileParser.h"
 #include "src/parser/LtlFileParser.h"
 
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-#include "log4cplus/consoleappender.h"
-#include "log4cplus/fileappender.h"
-log4cplus::Logger logger;
-
 #include "src/parser/PrismParser.h"
 #include "src/adapters/ExplicitModelAdapter.h"
 // #include "src/adapters/SymbolicModelAdapter.h"
 
 #include "src/exceptions/InvalidSettingsException.h"
 
-// Includes for the linked libraries and versions header
-#ifdef STORM_HAVE_INTELTBB
-#	include "tbb/tbb_stddef.h"
-#endif
-#ifdef STORM_HAVE_GLPK
-#	include "glpk.h"
-#endif
-#ifdef STORM_HAVE_GUROBI
-#	include "gurobi_c.h"
-#endif
-#ifdef STORM_HAVE_Z3
-#	include "z3.h"
-#endif
-
-#include <iostream>
-#include <iomanip>
-#include <fstream>
-
-void printUsage() {
-#ifndef WINDOWS	
-	struct rusage ru;
-	getrusage(RUSAGE_SELF, &ru);
-
-    std::cout << "===== Statistics ==============================" << std::endl;
-	std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl;
-	std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl;
-    std::cout << "===============================================" << std::endl;
-#else
-	HANDLE hProcess = GetCurrentProcess ();
-    FILETIME ftCreation, ftExit, ftUser, ftKernel;
-	PROCESS_MEMORY_COUNTERS pmc;
-	if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
-        std::cout << "Memory Usage: " << std::endl;
-		std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl;
-        std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl;
-        std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl;
-        std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl;
-        std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl;
-        std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl;
-        std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl;
-        std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl; 
-        std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl;
-    }
-
-	GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser);
-
-	ULARGE_INTEGER uLargeInteger;
-	uLargeInteger.LowPart = ftKernel.dwLowDateTime;
-	uLargeInteger.HighPart = ftKernel.dwHighDateTime;
-	double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
-	uLargeInteger.LowPart = ftUser.dwLowDateTime;
-	uLargeInteger.HighPart = ftUser.dwHighDateTime;
-	double userTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0;
-
-	std::cout << "CPU Time: " << std::endl;
-	std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl;
-	std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl;
-#endif
-}
-
-/*!
- * Initializes the logging framework and sets up logging to console.
- */
-void initializeLogger() {
-	logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main"));
-	logger.setLogLevel(log4cplus::INFO_LOG_LEVEL);
-	log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender());
-	consoleLogAppender->setName("mainConsoleAppender");
-	consoleLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL);
-	consoleLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n")));
-	logger.addAppender(consoleLogAppender);
-}
-
-/*!
- * Sets up the logging to file.
- */
-void setUpFileLogging() {
-	storm::settings::Settings* s = storm::settings::Settings::getInstance();
-	log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(s->getOptionByLongName("logfile").getArgument(0).getValueAsString()));
-	fileLogAppender->setName("mainFileAppender");
-	fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n")));
-	logger.addAppender(fileLogAppender);
-}
-
-/*!
-* Gives the current working directory
-*
-* @return std::string The path of the current working directory
-*/
-std::string getCurrentWorkingDirectory() {
-	char temp[512];
-	return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string(""));
-}
-
-/*!
- * Prints the header.
- */
-void printHeader(const int argc, const char* argv[]) {
-	std::cout << "StoRM" << std::endl;
-	std::cout << "-----" << std::endl << std::endl;
-
-	std::cout << "Version: " << STORM_CPP_VERSION_MAJOR << "." << STORM_CPP_VERSION_MINOR << "." << STORM_CPP_VERSION_PATCH;
-	if (STORM_CPP_VERSION_COMMITS_AHEAD != 0) {
-		std::cout << " (+" << STORM_CPP_VERSION_COMMITS_AHEAD << " commits)";
-	}
-	std::cout << " build from revision " << STORM_CPP_VERSION_HASH;
-	if (STORM_CPP_VERSION_DIRTY == 1) {
-		std::cout << " (DIRTY)";
-	}
-	std::cout << "." << std::endl;
-	
-#ifdef STORM_HAVE_INTELTBB
-	std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
-#endif
-#ifdef STORM_HAVE_GLPK
-	std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl;
-#endif
-#ifdef STORM_HAVE_GUROBI
-	std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl;
-#endif
-#ifdef STORM_HAVE_Z3
-	unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
-	Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
-	std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl;
-#endif
-    
-	// "Compute" the command line argument string with which STORM was invoked.
-	std::stringstream commandStream;
-	for (int i = 0; i < argc; ++i) {
-		commandStream << argv[i] << " ";
-	}
-	std::cout << "Command line: " << commandStream.str() << std::endl << std::endl;
-	std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
-}
-
-/*!
- * Parses the given command line arguments.
- *
- * @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(const int argc, const char* argv[]) {
-	storm::settings::Settings* s = storm::settings::Settings::getInstance();
-	try {
-		storm::settings::Settings::parse(argc, argv);
-	} catch (storm::exceptions::OptionParserException& e) {
-		std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
-		std::cout << std::endl << s->getHelpText();
-		return false;
-	}
-
-	if (s->isSet("help")) {
-		std::cout << storm::settings::Settings::getInstance()->getHelpText();
-		return false;
-	}
-
-	if (s->isSet("verbose")) {
-		logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
-		LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console.");
-	}
-	if (s->isSet("debug")) {
-		logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL);
-		logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL);
-		LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console.");
-	}
-	if (s->isSet("trace")) {
-		logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL);
-		logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL);
-		LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console.");
-	}
-	if (s->isSet("logfile")) {
-		setUpFileLogging();
-	}
-	return true;
-}
-
-/*!
- * Performs some necessary initializations.
- */
-void setUp() {
-    // Increase the precision of output.
-	std::cout.precision(10);
-}
-
-/*!
- * Performs some necessary clean-up.
- */
-void cleanUp() {
-    // Intentionally left empty.
-}
 
-/*!
- * Creates a model checker for the given DTMC that complies with the given options.
- *
- * @param dtmc A reference to the DTMC for which the model checker is to be created.
- * @return A pointer to the resulting model checker.
- */
-storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Dtmc<double> const & dtmc) {
-    // Create the appropriate model checker.
-	storm::settings::Settings* s = storm::settings::Settings::getInstance();
-	std::string const& linsolver = s->getOptionByLongName("linsolver").getArgument(0).getValueAsString();
-	if (linsolver == "gmm++") {
-		return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
-	} else if (linsolver == "native") {
-		return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc, new storm::solver::NativeLinearEquationSolver<double>());
-    }
-    
-	// The control flow should never reach this point, as there is a default setting for matrixlib.
-	std::string message = "No matrix library suitable for DTMC model checking has been set.";
-	throw storm::exceptions::InvalidSettingsException() << message;
-	return nullptr;
-}
 
-/*!
- * Creates a model checker for the given MDP that complies with the given options.
- *
- * @param mdp The Dtmc that the model checker will check
- * @return
- */
-storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Mdp<double> const & mdp) {
-    // Create the appropriate model checker.
-    return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp);
-}
 
 /*!
  * Checks the PRCTL formulae provided on the command line on the given model checker.
@@ -312,131 +87,6 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
 	}
 }
 
-/*!
- * Handles the counterexample generation control.
- *
- * @param parser An AutoParser to get the model from.
- */
- void generateCounterExample(std::shared_ptr<storm::models::AbstractModel<double>> model) {
-	LOG4CPLUS_INFO(logger, "Starting counterexample generation.");
-	LOG4CPLUS_INFO(logger, "Testing inputs...");
-
-	storm::settings::Settings* s  = storm::settings::Settings::getInstance();
-
-	// First test output directory.
-	std::string outPath = s->getOptionByLongName("counterExample").getArgument(0).getValueAsString();
-	if(outPath.back() != '/' && outPath.back() != '\\') {
-		LOG4CPLUS_ERROR(logger, "The output path is not valid.");
-		return;
-	}
-	std::ofstream testFile(outPath + "test.dot");
-	if(testFile.fail()) {
-		LOG4CPLUS_ERROR(logger, "The output path is not valid.");
-		return;
-	}
-	testFile.close();
-	std::remove((outPath + "test.dot").c_str());
-
- 	// Differentiate between model types.
-	if(model->getType() != storm::models::DTMC) {
-		LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported.");
-		return;
-	}
-
-	// Get the Dtmc back from the AbstractModel
-	// Note that the ownership of the object referenced by dtmc lies at the main function.
-	// Thus, it must not be deleted.
-	storm::models::Dtmc<double> dtmc = *(model->as<storm::models::Dtmc<double>>());
-	LOG4CPLUS_INFO(logger, "Model is a DTMC.");
-
-	// Get specified PRCTL formulas.
-	if(!s->isSet("prctl")) {
-		LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified.");
-		return;
-	}
-
-	std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString();
-	LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << ".");
-	std::list<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile);
-
-	// Test for each formula if a counterexample can be generated for it.
-	if(formulaList.size() == 0) {
-		LOG4CPLUS_ERROR(logger, "No PRCTL formula found.");
-		return;
-	}
-
-	// Get prctl file name without the filetype
-	uint_fast64_t first = 0;
-	if(chosenPrctlFile.find('/') != std::string::npos) {
-		first = chosenPrctlFile.find_last_of('/') + 1;
-	} else if(chosenPrctlFile.find('\\') != std::string::npos) {
-		first = chosenPrctlFile.find_last_of('\\') + 1;
-	}
-
-	uint_fast64_t length;
-	if(chosenPrctlFile.find_last_of('.') != std::string::npos && chosenPrctlFile.find_last_of('.') >= first) {
-		length = chosenPrctlFile.find_last_of('.') - first;
-	} else {
-		length = chosenPrctlFile.length() - first;
-	}
-
-	std::string outFileName = chosenPrctlFile.substr(first, length);
-
-	// Test formulas and do generation
-	uint_fast64_t fIndex = 0;
-	for (auto formula : formulaList) {
-
-		// First check if it is a formula type for which a counterexample can be generated.
-		if (std::dynamic_pointer_cast<storm::properties::prctl::AbstractStateFormula<double>>(formula->getChild()).get() == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula.");
-			continue;
-		}
-
-		std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>> stateForm = std::static_pointer_cast<storm::properties::prctl::AbstractStateFormula<double>>(formula->getChild());
-
-		// Do some output
-		std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl;
-		LOG4CPLUS_INFO(logger, "Generating counterexample for formula " + std::to_string(fIndex) + ": ");
-		std::cout << "\t" << formula->toString() << "\n" << std::endl;
-		LOG4CPLUS_INFO(logger, formula->toString());
-
-		// Now check if the model does not satisfy the formula.
-		// That is if there is at least one initial state of the model that does not.
-
-		// Also raise the logger threshold for the log file, so that the model check infos aren't logged (useless and there are lots of them)
-		// Lower it again after the model check.
-		logger.getAppender("mainFileAppender")->setThreshold(log4cplus::WARN_LOG_LEVEL);
-		storm::storage::BitVector result = stateForm->check(*createPrctlModelChecker(dtmc));
-		logger.getAppender("mainFileAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
-
-		if((result & dtmc.getInitialStates()).getNumberOfSetBits() == dtmc.getInitialStates().getNumberOfSetBits()) {
-			std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl;
-			LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample.");
-			continue;
-		}
-
-		// Generate counterexample
-		storm::models::Dtmc<double> counterExample = storm::counterexamples::PathBasedSubsystemGenerator<double>::computeCriticalSubsystem(dtmc, stateForm);
-
-		LOG4CPLUS_INFO(logger, "Found counterexample.");
-
-		// Output counterexample
-		// Do standard output
-		std::cout << "Found counterexample with following properties: " << std::endl;
-		counterExample.printModelInformationToStream(std::cout);
-		std::cout << "For full Dtmc see " << outFileName << "_" << fIndex << ".dot at given output path.\n\n" << std::endl;
-
-		// Write the .dot file
-		std::ofstream outFile(outPath + outFileName + "_" + std::to_string(fIndex) + ".dot");
-		if(outFile.good()) {
-			counterExample.writeDotToStream(outFile, true, nullptr, nullptr, nullptr, nullptr, nullptr, nullptr, true);
-			outFile.close();
-		}
-
-		fIndex++;
-	}
- }
-
 /*!
  * Main entry point.
  */

src/utility/CLI.h

@@ -0,0 +1,168 @@
+#ifndef STORM_UTILITY_CLI_H_
+#define STORM_UTILITY_CLI_H_
+
+#include <iostream>
+#include <fstream>
+#include <cstdio>
+#include <sstream>
+
+
+#include "src/utility/OsDetection.h"
+// Registers all standard options
+#include "src/utility/StormOptions.h" 
+
+
+// Includes for the linked libraries and versions header
+#ifdef STORM_HAVE_INTELTBB
+#	include "tbb/tbb_stddef.h"
+#endif
+#ifdef STORM_HAVE_GLPK
+#	include "glpk.h"
+#endif
+#ifdef STORM_HAVE_GUROBI
+#	include "gurobi_c.h"
+#endif
+#ifdef STORM_HAVE_Z3
+#	include "z3.h"
+#endif
+
+/*!
+* Gives the current working directory
+*
+* @return std::string The path of the current working directory
+*/
+std::string getCurrentWorkingDirectory() {
+	char temp[512];
+	return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string(""));
+}
+
+
+void printUsage() {
+#ifndef WINDOWS	
+	struct rusage ru;
+	getrusage(RUSAGE_SELF, &ru);
+
+    std::cout << "===== Statistics ==============================" << std::endl;
+	std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl;
+	std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl;
+    std::cout << "===============================================" << std::endl;
+#else
+	HANDLE hProcess = GetCurrentProcess ();
+    FILETIME ftCreation, ftExit, ftUser, ftKernel;
+	PROCESS_MEMORY_COUNTERS pmc;
+	if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
+        std::cout << "Memory Usage: " << std::endl;
+		std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl;
+        std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl;
+        std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl;
+        std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl;
+        std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl;
+        std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl;
+        std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl;
+        std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl; 
+        std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl;
+    }
+
+	GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser);
+
+	ULARGE_INTEGER uLargeInteger;
+	uLargeInteger.LowPart = ftKernel.dwLowDateTime;
+	uLargeInteger.HighPart = ftKernel.dwHighDateTime;
+	double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
+	uLargeInteger.LowPart = ftUser.dwLowDateTime;
+	uLargeInteger.HighPart = ftUser.dwHighDateTime;
+	double userTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0;
+
+	std::cout << "CPU Time: " << std::endl;
+	std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl;
+	std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl;
+#endif
+}
+
+
+
+/*!
+ * Prints the header.
+ */
+void printHeader(const int argc, const char* argv[]) {
+	std::cout << "StoRM" << std::endl;
+	std::cout << "-----" << std::endl << std::endl;
+
+	std::cout << "Version: " << STORM_CPP_VERSION_MAJOR << "." << STORM_CPP_VERSION_MINOR << "." << STORM_CPP_VERSION_PATCH;
+	if (STORM_CPP_VERSION_COMMITS_AHEAD != 0) {
+		std::cout << " (+" << STORM_CPP_VERSION_COMMITS_AHEAD << " commits)";
+	}
+	std::cout << " build from revision " << STORM_CPP_VERSION_HASH;
+	if (STORM_CPP_VERSION_DIRTY == 1) {
+		std::cout << " (DIRTY)";
+	}
+	std::cout << "." << std::endl;
+	
+#ifdef STORM_HAVE_INTELTBB
+	std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
+#endif
+#ifdef STORM_HAVE_GLPK
+	std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl;
+#endif
+#ifdef STORM_HAVE_GUROBI
+	std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl;
+#endif
+#ifdef STORM_HAVE_Z3
+	unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
+	Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
+	std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl;
+#endif
+    
+	// "Compute" the command line argument string with which STORM was invoked.
+	std::stringstream commandStream;
+	for (int i = 0; i < argc; ++i) {
+		commandStream << argv[i] << " ";
+	}
+	std::cout << "Command line: " << commandStream.str() << std::endl << std::endl;
+	std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
+}
+
+/*!
+ * Parses the given command line arguments.
+ *
+ * @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(const int argc, const char* argv[]) {
+	storm::settings::Settings* s = storm::settings::Settings::getInstance();
+	try {
+		storm::settings::Settings::parse(argc, argv);
+	} catch (storm::exceptions::OptionParserException& e) {
+		std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
+		std::cout << std::endl << s->getHelpText();
+		return false;
+	}
+
+	if (s->isSet("help")) {
+		std::cout << storm::settings::Settings::getInstance()->getHelpText();
+		return false;
+	}
+
+	if (s->isSet("verbose")) {
+		logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
+		LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console.");
+	}
+	if (s->isSet("debug")) {
+		logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL);
+		logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL);
+		LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console.");
+	}
+	if (s->isSet("trace")) {
+		logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL);
+		logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL);
+		LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console.");
+	}
+	if (s->isSet("logfile")) {
+		setUpFileLogging();
+	}
+	return true;
+}
+
+
+#endif

src/utility/Initialize.h

@@ -0,0 +1,22 @@
+#ifndef STORM_UTILITY_INITIALIZE_H_
+#define STORM_UTILITY_INITIALIZE_H_
+
+#include "InitializeLogging.h"
+
+/*!
+ * Performs some necessary initializations.
+ */
+void setUp() {
+    // Increase the precision of output.
+	std::cout.precision(10);
+}
+
+/*!
+ * Performs some necessary clean-up.
+ */
+void cleanUp() {
+    // Intentionally left empty.
+}
+
+
+#endif

src/utility/InitializeLogging.h

@@ -0,0 +1,38 @@
+#ifndef STORM_UTILITY_INITIALIZELOGGING_H_
+#define STORM_UTILITY_INITIALIZELOGGING_H_
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+#include "log4cplus/consoleappender.h"
+#include "log4cplus/fileappender.h"
+
+#include "src/settings/Settings.h"
+
+log4cplus::Logger logger;
+
+/*!
+ * Initializes the logging framework and sets up logging to console.
+ */
+void initializeLogger() {
+	logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main"));
+	logger.setLogLevel(log4cplus::INFO_LOG_LEVEL);
+	log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender());
+	consoleLogAppender->setName("mainConsoleAppender");
+	consoleLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL);
+	consoleLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n")));
+	logger.addAppender(consoleLogAppender);
+}
+
+/*!
+ * Sets up the logging to file.
+ */
+void setUpFileLogging() {
+	storm::settings::Settings* s = storm::settings::Settings::getInstance();
+	log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(s->getOptionByLongName("logfile").getArgument(0).getValueAsString()));
+	fileLogAppender->setName("mainFileAppender");
+	fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n")));
+	logger.addAppender(fileLogAppender);
+}
+
+
+#endif

src/utility/cstring.cpp

@@ -22,8 +22,8 @@ namespace cstring {
  *	@param end New pointer will be written there
  *	@return Result of strtol()
  */
-uint_fast64_t checked_strtol(const char* str, char** end) {
-	uint_fast64_t res = strtol(str, end, 10);
+uint_fast64_t checked_strtol(char const* str, char const** end) {
+	uint_fast64_t res = strtol(str, const_cast<char**>(end), 10);
 	if (str == *end) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing integer. Next input token is not a number.");
 		LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\"");
@@ -40,8 +40,8 @@ uint_fast64_t checked_strtol(const char* str, char** end) {
  *	@param end New pointer will be written there
  *	@return Result of strtod()
  */
-double checked_strtod(const char* str, char** end) {
-	double res = strtod(str, end);
+double checked_strtod(char const* str, char const** end) {
+	double res = strtod(str, const_cast<char**>(end));
 	if (str == *end) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing floating point. Next input token is not a number.");
 		LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\"");
@@ -56,7 +56,7 @@ double checked_strtod(const char* str, char** end) {
  * @param buf The string buffer to operate on.
  * @return A pointer to the first whitespace character.
  */
-char* skipWord(char* buf){
+char const* skipWord(char const* buf){
 	while(!isspace(*buf) && *buf != '\0') buf++;
 	return buf;
 }
@@ -67,7 +67,7 @@ char* skipWord(char* buf){
  *	@param buf The string buffer to operate on.
  *	@return	A pointer to the first non-whitespace character.
  */
-char* trimWhitespaces(char* buf) {
+char const* trimWhitespaces(char const* buf) {
 	while (isspace(*buf)) buf++;
 	return buf;
 }
@@ -75,15 +75,15 @@ char* trimWhitespaces(char* buf) {
 /*!
  * @brief Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newline character).
  */
-char* forwardToLineEnd(char* buffer) {
+char const* forwardToLineEnd(char const* buffer) {
 	return buffer + strcspn(buffer, "\n\r\0");
 }
 
 /*!
  * @brief Encapsulates the usage of function @strchr to forward to the next line
  */
-char* forwardToNextLine(char* buffer) {
-	char* lineEnd = forwardToLineEnd(buffer);
+char const* forwardToNextLine(char const* buffer) {
+	char const* lineEnd = forwardToLineEnd(buffer);
 	while((*lineEnd == '\n') || (*lineEnd == '\r')) lineEnd++;
 	return lineEnd;
 }

src/utility/cstring.h

@@ -17,34 +17,34 @@ namespace storm {
 		/*!
 		 *	@brief Parses integer and checks, if something has been parsed.
 		 */
-		uint_fast64_t checked_strtol(const char* str, char** end);
+		uint_fast64_t checked_strtol(const char* str, char const** end);
 
 		/*!
 		 *	@brief Parses floating point and checks, if something has been parsed.
 		 */
-		double checked_strtod(const char* str, char** end);
+		double checked_strtod(const char* str, char const** end);
 
 		/*!
 		 * @brief Skips all non whitespace characters until the next whitespace.
 		 */
-		char* skipWord(char* buf);
+		char const* skipWord(char const* buf);
 
 		/*!
 		 *	@brief Skips common whitespaces in a string.
 		 */
-		char* trimWhitespaces(char* buf);
+		char const* trimWhitespaces(char const* buf);
 
 		/*!
 		 * @brief Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newline character).
 		 */
-		char* forwardToLineEnd(char* buffer);
+		char const* forwardToLineEnd(char const* buffer);
 
 		/*!
 		 * @brief Encapsulates the usage of function @strchr to forward to the next line
 		 *
 		 * Note: All lines after the current, which do not contain any characters are skipped.
 		 */
-		char* forwardToNextLine(char* buffer);
+		char const* forwardToNextLine(char const* buffer);
 
 		} // namespace cstring
 	} // namespace utility

test/functional/parser/MappedFileTest.cpp

@@ -23,8 +23,8 @@ TEST(MappedFileTest, BasicFunctionality) {
 	// Open a file and test if the content is loaded as expected.
 	storm::parser::MappedFile file(STORM_CPP_TESTS_BASE_PATH "/functional/parser/testStringFile.txt");
 	std::string testString = "This is a test string.";
-	char * dataPtr = file.getData();
-	for(char const * testStringPtr = testString.c_str(); testStringPtr - testString.c_str() < 22; testStringPtr++) {
+	char const* dataPtr = file.getData();
+	for(char const* testStringPtr = testString.c_str(); testStringPtr - testString.c_str() < 22; testStringPtr++) {
 		ASSERT_EQ(*testStringPtr, *dataPtr);
 		dataPtr++;
 	}

test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp

@@ -5,7 +5,7 @@
 #include "src/settings/Settings.h"
 
 TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
-    storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
+    storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true);
     ASSERT_NO_THROW(builder.newRowGroup(0));
     ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
 
@@ -24,7 +24,7 @@ TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
 }
 
 TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
-    storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
+    storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true);
     ASSERT_NO_THROW(builder.newRowGroup(0));
     ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
     ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099));

test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp

@@ -5,7 +5,7 @@
 #include "src/settings/Settings.h"
 
 TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
-    storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
+    storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true);
     ASSERT_NO_THROW(builder.newRowGroup(0));
     ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
     
@@ -24,7 +24,7 @@ TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
 }
 
 TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
-    storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
+    storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true);
     ASSERT_NO_THROW(builder.newRowGroup(0));
     ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
     ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099));

test/functional/storage/SparseMatrixTest.cpp

@@ -221,7 +221,7 @@ TEST(SparseMatrix, MakeAbsorbing) {
 }
 
 TEST(SparseMatrix, MakeRowGroupAbsorbing) {
-    storm::storage::SparseMatrixBuilder<double> matrixBuilder(5, 4, 9, true);
+    storm::storage::SparseMatrixBuilder<double> matrixBuilder(5, 4, 9, true, true);
     ASSERT_NO_THROW(matrixBuilder.newRowGroup(0));
     ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0));
     ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2));
@@ -242,7 +242,7 @@ TEST(SparseMatrix, MakeRowGroupAbsorbing) {
     
     ASSERT_NO_THROW(matrix.makeRowGroupsAbsorbing(absorbingRowGroups));
 
-    storm::storage::SparseMatrixBuilder<double> matrixBuilder2(0, 0, 0, true);
+    storm::storage::SparseMatrixBuilder<double> matrixBuilder2(0, 0, 0, false, true);
     ASSERT_NO_THROW(matrixBuilder2.newRowGroup(0));
     ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0));
     ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2));
@@ -283,7 +283,7 @@ TEST(SparseMatrix, ConstrainedRowSumVector) {
     std::vector<double> constrainedRowSum = matrix.getConstrainedRowSumVector(storm::storage::BitVector(5, true), columnConstraint);
     ASSERT_TRUE(constrainedRowSum == std::vector<double>({1.0, 0.7, 0, 0, 0.5}));
     
-    storm::storage::SparseMatrixBuilder<double> matrixBuilder2(5, 4, 9, true);
+    storm::storage::SparseMatrixBuilder<double> matrixBuilder2(5, 4, 9, true, true);
     ASSERT_NO_THROW(matrixBuilder2.newRowGroup(0));
     ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0));
     ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2));
@@ -312,7 +312,7 @@ TEST(SparseMatrix, ConstrainedRowSumVector) {
 }
 
 TEST(SparseMatrix, Submatrix) {
-    storm::storage::SparseMatrixBuilder<double> matrixBuilder(5, 4, 9, true);
+    storm::storage::SparseMatrixBuilder<double> matrixBuilder(5, 4, 9, true, true);
     ASSERT_NO_THROW(matrixBuilder.newRowGroup(0));
     ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0));
     ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2));
@@ -342,7 +342,7 @@ TEST(SparseMatrix, Submatrix) {
     ASSERT_NO_THROW(storm::storage::SparseMatrix<double> matrix2 = matrix.getSubmatrix(true, rowGroupConstraint, columnConstraint, false));
     storm::storage::SparseMatrix<double> matrix2 = matrix.getSubmatrix(true, rowGroupConstraint, columnConstraint, false);
     
-    storm::storage::SparseMatrixBuilder<double> matrixBuilder3(3, 2, 3, true);
+    storm::storage::SparseMatrixBuilder<double> matrixBuilder3(3, 2, 3, true, true);
     ASSERT_NO_THROW(matrixBuilder3.newRowGroup(0));
     ASSERT_NO_THROW(matrixBuilder3.addNextValue(0, 0, 0.5));
     ASSERT_NO_THROW(matrixBuilder3.newRowGroup(2));

test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp

@@ -15,7 +15,7 @@ TEST(StronglyConnectedComponentDecomposition, Crowds) {
     ASSERT_EQ(1290297ull, sccDecomposition.size());
 
     ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true));
-    ASSERT_EQ(1290297, sccDecomposition.size());
+    ASSERT_EQ(437690, sccDecomposition.size());
 
     ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true, true));
     ASSERT_EQ(425040, sccDecomposition.size());
@@ -33,7 +33,7 @@ TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) {
     ASSERT_EQ(2611835, sccDecomposition.size());
 
     ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true));
-    ASSERT_EQ(2611835, sccDecomposition.size());
+    ASSERT_EQ(2, sccDecomposition.size());
 
     ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true, true));
     ASSERT_EQ(1, sccDecomposition.size());