Edited all Parsers to lose its class.

Modified many classes to provide a reference-constructor.
Fixed a few bugs in Tests.


Former-commit-id: c31fe95aae

resources/3rdparty/ltl2dstar-0.5.1/src/APMonom.hpp

@@ -29,6 +29,10 @@
 #include <cassert>
 #include <iostream>
 
+// As TRUE and FALSE are defined to equal true and false on Windows, they need to be undefined.
+#undef TRUE
+#undef FALSE
+
 /**
  * Class representing a subset of 2^AP where AP is the set of 
  * atomic propositions (APSet). It stores two bits per AP: 

src/models/AbstractModel.h

@@ -71,7 +71,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 			}
 
 			if (optionalTransitionRewardMatrix) { // Boost::Optional
-				this->stateRewardVector.reset(new storm::storage::SparseMatrix<T>(optionalTransitionRewardMatrix.get()));
+				this->transitionRewardMatrix.reset(new storm::storage::SparseMatrix<T>(optionalTransitionRewardMatrix.get()));
 			}
 		}
 

src/models/AbstractNondeterministicModel.h

@@ -35,6 +35,25 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
 			  nondeterministicChoiceIndices(nondeterministicChoiceIndices) {
 		}
 
+		/*! Constructs an abstract non-determinstic model from the given parameters.
+		 * All values are copied.
+		 * @param transitionMatrix The matrix representing the transitions in the model.
+		 * @param stateLabeling The labeling that assigns a set of atomic
+		 * propositions to each state.
+		 * @param choiceIndices A mapping from states to rows in the transition matrix.
+		 * @param stateRewardVector The reward values associated with the states.
+		 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
+		 */
+		AbstractNondeterministicModel(
+			storm::storage::SparseMatrix<T> const& transitionMatrix, 
+			storm::models::AtomicPropositionsLabeling const& stateLabeling,
+			std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
+			boost::optional<std::vector<T>> const& optionalStateRewardVector, 
+			boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix)
+			: AbstractModel<T>(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) {
+				this->nondeterministicChoiceIndices.reset(new std::vector<uint_fast64_t>(nondeterministicChoiceIndices));
+		}
+
 		/*!
 		 * Destructor.
 		 */

src/models/Ctmdp.h

@@ -49,6 +49,27 @@ public:
 		}
 	}
 
+	/*!
+	 * Constructs a CTMDP object from the given transition probability matrix and
+	 * the given labeling of the states.
+	 * All values are copied.
+	 * @param probabilityMatrix The transition probability relation of the
+	 * CTMDP given by a matrix.
+	 * @param stateLabeling The labeling that assigns a set of atomic
+	 * propositions to each state.
+	 */
+	Ctmdp(storm::storage::SparseMatrix<T> const& probabilityMatrix, 
+			storm::models::AtomicPropositionsLabeling const& stateLabeling,
+			std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
+			boost::optional<std::vector<T>> const& optionalStateRewardVector, 
+			boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix)
+			: AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix) {
+		if (!this->checkValidityOfProbabilityMatrix()) {
+			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
+			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
+		}
+	}
+
 	//! Copy Constructor
 	/*!
 	 * Copy Constructor. Performs a deep copy of the given CTMDP.

src/models/Dtmc.h

@@ -74,8 +74,8 @@ public:
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
 		}
-		if (this->getTransitionRewardMatrix() != nullptr) {
-			if (!this->getTransitionRewardMatrix()->containsAllPositionsOf(*this->getTransitionMatrix())) {
+		if (this->hasTransitionRewards()) {
+			if (!this->getTransitionRewardMatrix().containsAllPositionsOf(this->getTransitionMatrix())) {
 				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.";
 			}

src/models/Mdp.h

@@ -51,6 +51,27 @@ public:
 		}
 	}
 
+	/*!
+	 * Constructs a MDP object from the given transition probability matrix and
+	 * the given labeling of the states.
+	 * All values are copied.
+	 * @param probabilityMatrix The transition probability relation of the
+	 * MDP given by a matrix.
+	 * @param stateLabeling The labeling that assigns a set of atomic
+	 * propositions to each state.
+	 */
+	Mdp(storm::storage::SparseMatrix<T> const& transitionMatrix, 
+			storm::models::AtomicPropositionsLabeling const& stateLabeling,
+			std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
+			boost::optional<std::vector<T>> const& optionalStateRewardVector, 
+			boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix)
+			: AbstractNondeterministicModel<T>(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix) {
+		if (!this->checkValidityOfProbabilityMatrix()) {
+			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
+			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
+		}
+	}
+
 	//! Copy Constructor
 	/*!
 	 * Copy Constructor. Performs a deep copy of the given MDP.

src/parser/AtomicPropositionLabelingParser.cpp

@@ -44,9 +44,9 @@ storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_f
 	/*
 	 *	Open file.
 	 */
-	if (!fileExistsAndIsReadable(filename.c_str())) {
+	if (!storm::parser::fileExistsAndIsReadable(filename.c_str())) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
-		throw storm::exceptions::WrongFormatException();
+		throw storm::exceptions::FileIoException() << "The supplied Labeling input file \"" << filename << "\" does not exist or is not readable by this process.";
 	}
 
 	MappedFile file(filename.c_str());

src/parser/AutoParser.h

@@ -30,7 +30,7 @@ namespace parser {
  *	can be obtained via getType() and getModel<ModelClass>().
  */
 template<class T>
-class AutoParser : Parser {
+class AutoParser {
 	public:
 		AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile,
 				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "") : model(nullptr) {
@@ -47,23 +47,19 @@ class AutoParser : Parser {
 			// Do actual parsing
 			switch (type) {
 				case storm::models::DTMC: {
-					DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-					this->model = parser.getDtmc();
+					this->model.reset(new storm::models::Dtmc<double>(DeterministicModelParserAsDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
 					break;
 				}
 				case storm::models::CTMC: {
-					DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-					this->model = parser.getCtmc();
+					this->model.reset(new storm::models::Ctmc<double>(DeterministicModelParserAsCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
 					break;
 				}
 				case storm::models::MDP: {
-					NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-					this->model = parser.getMdp();
+					this->model.reset(new storm::models::Mdp<double>(NondeterministicModelParserAsMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
 					break;
 				}
 				case storm::models::CTMDP: {
-					NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-					this->model = parser.getCtmdp();
+					this->model.reset(new storm::models::Ctmdp<double>(NondeterministicModelParserAsCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
 					break;
 				}
 				default: ;  // Unknown
@@ -71,7 +67,7 @@ class AutoParser : Parser {
 
 
 			if (!this->model) {
-				LOG4CPLUS_WARN(logger, "Model is still null.");
+				LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type. Model is still null.");
 			}
 		}
 		
@@ -101,13 +97,44 @@ class AutoParser : Parser {
 		 */
 		storm::models::ModelType analyzeHint(const std::string& filename) {
 			storm::models::ModelType hintType = storm::models::Unknown;
+			
+			// Parse the File and check for the Line Endings
+			storm::parser::SupportedLineEndingsEnum lineEndings = storm::parser::findUsedLineEndings(filename);
+			
 			// Open file
 			MappedFile file(filename.c_str());
 			char* buf = file.data;
 
 			// parse hint
 			char hint[128];
-			sscanf(buf, "%s\n", hint);
+			// %20s => The Input Hint can be AT MOST 120 chars long			
+			switch (lineEndings) {
+				case storm::parser::SupportedLineEndingsEnum::SlashN:
+#ifdef WINDOWS					
+					sscanf_s(buf, "%120s\n", hint, sizeof(hint));
+#else
+					sscanf(buf, "%120s\n", hint);
+#endif
+					break;
+				case storm::parser::SupportedLineEndingsEnum::SlashR:
+#ifdef WINDOWS					
+					sscanf_s(buf, "%120s\r", hint, sizeof(hint));
+#else
+					sscanf(buf, "%120s\r", hint);
+#endif
+					break;
+				case storm::parser::SupportedLineEndingsEnum::SlashRN:
+#ifdef WINDOWS					
+					sscanf_s(buf, "%120s\r\n", hint, sizeof(hint));
+#else
+					sscanf(buf, "%120s\r\n", hint);
+#endif
+					break;
+				default:
+					LOG4CPLUS_ERROR(logger, "The given input file \"" << filename << "\" has no or unsupported line endings. Please use either \\r, \\n or \\r\\n.");
+					throw storm::exceptions::WrongFormatException() << "The given input file \"" << filename << "\" has no or unsupported line endings. Please use either \\r, \\n or \\r\\n.";
+			}
+
 			for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
 
 			// check hint

src/parser/DeterministicSparseTransitionParser.cpp

@@ -139,7 +139,7 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::st
 
 	if (!fileExistsAndIsReadable(filename.c_str())) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
-		throw storm::exceptions::WrongFormatException();
+		throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process.";
 	}
 
 	/*

src/parser/LtlFileParser.cpp

@@ -11,16 +11,7 @@
 namespace storm {
 namespace parser {
 
-LtlFileParser::LtlFileParser() {
-	// TODO Auto-generated constructor stub
-
-}
-
-LtlFileParser::~LtlFileParser() {
-	// TODO Auto-generated destructor stub
-}
-
-std::list<storm::property::ltl::AbstractLtlFormula<double>*> LtlFileParser::parseFormulas(std::string filename) {
+std::list<storm::property::ltl::AbstractLtlFormula<double>*> LtlFileParser(std::string filename) {
 	// Open file
 	std::ifstream inputFileStream(filename, std::ios::in);
 
@@ -35,8 +26,7 @@ std::list<storm::property::ltl::AbstractLtlFormula<double>*> LtlFileParser::pars
 		std::string line;
 		//The while loop reads the input file line by line
 		while (std::getline(inputFileStream, line)) {
-			LtlParser parser(line);
-			result.push_back(parser.getFormula());
+			result.push_back(storm::parser::LtlParser(line));
 		}
 	}
 

src/parser/LtlFileParser.h

@@ -15,26 +15,13 @@
 namespace storm {
 namespace parser {
 
-class LtlFileParser {
-public:
-	/*!
-	 * Constructor
-	 */
-	LtlFileParser();
-
-	/*!
-	 * Destructor
-	 */
-	~LtlFileParser();
-
-	/*!
-	 * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
-	 *
-	 * @param filename
-	 * @return The list of parsed formulas
-	 */
-	std::list<storm::property::ltl::AbstractLtlFormula<double>*> parseFormulas(std::string filename);
-};
+/*!
+ * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
+ *
+ * @param filename
+ * @return The list of parsed formulas
+ */
+std::list<storm::property::ltl::AbstractLtlFormula<double>*> LtlFileParser(std::string filename);
 
 } //namespace parser
 } //namespace storm

src/parser/NondeterministicModelParser.cpp

@@ -18,8 +18,7 @@ namespace storm {
 namespace parser {
 
 /*!
- * Parses a transition file and a labeling file and produces a MDP out of them; a pointer to the mdp
- * is saved in the field "mdp"
+ * Parses a transition file and a labeling file and produces an intermediate Result Container
  * Note that the labeling file may have at most as many nodes as the transition file!
  *
  * @param transitionSystemFile String containing the location of the transition file (....tra)
@@ -27,27 +26,49 @@ 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)
  */
-NondeterministicModelParser::NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+NondeterministicModelParserResultContainer<double> parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
 		std::string const & stateRewardFile, std::string const & transitionRewardFile) {
+
 	NondeterministicSparseTransitionParserResult_t nondeterministicSparseTransitionParserResult = storm::parser::NondeterministicSparseTransitionParser(transitionSystemFile);
-	uint_fast64_t stateCount = nondeterministicSparseTransitionParserResult.first.getColumnCount();
+	storm::storage::SparseMatrix<double> resultTransitionSystem = nondeterministicSparseTransitionParserResult.first;
+
+	uint_fast64_t stateCount = resultTransitionSystem.getRowCount();
+
+	storm::models::AtomicPropositionsLabeling resultLabeling = storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile);
 
+	NondeterministicModelParserResultContainer<double> result(resultTransitionSystem, nondeterministicSparseTransitionParserResult.second, resultLabeling);
+	
 	if (stateRewardFile != "") {
-		std::vector<double> stateRewards = storm::parser::SparseStateRewardParser(stateCount, stateRewardFile);
+		result.stateRewards.reset(storm::parser::SparseStateRewardParser(stateCount, stateRewardFile));
 	}
 	if (transitionRewardFile != "") {
-		RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(nondeterministicSparseTransitionParserResult.first.getRowCount(), nondeterministicSparseTransitionParserResult.first.getColumnCount(), nondeterministicSparseTransitionParserResult.second);
-		storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, rewardMatrixInfo);
+		RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(nondeterministicSparseTransitionParserResult.first.getRowCount(), nondeterministicSparseTransitionParserResult.first.getColumnCount(), &nondeterministicSparseTransitionParserResult.second);
+		result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser(transitionRewardFile, rewardMatrixInfo).first);
 		delete rewardMatrixInfo;
-		this->transitionRewardMatrix = trp.getMatrix();
 	}
+	return result;
+}
 
-	this->probabilityMatrix = tp.getMatrix();
-	this->stateLabeling = std::shared_ptr<storm::models::AtomicPropositionsLabeling>(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile));
-	this->rowMapping = tp.getRowMapping();
+/*!
+ * Uses the Function parseNondeterministicModel internally to parse the given input files.
+ * @note This is a Short-Hand for Constructing a Mdp directly from the data returned by @parseNondeterministicModel
+ * @return A Mdp Model
+ */
+storm::models::Mdp<double> NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile,
+														 std::string const & stateRewardFile, std::string const & transitionRewardFile) {
+	NondeterministicModelParserResultContainer<double> parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+	return storm::models::Mdp<double>(parserResult.transitionSystem, parserResult.labeling, parserResult.rowMapping, parserResult.stateRewards, parserResult.transitionRewards);
+}
 
-	this->mdp = nullptr;
-	this->ctmdp = nullptr;
+/*!
+ * Uses the Function parseNondeterministicModel internally to parse the given input files.
+ * @note This is a Short-Hand for Constructing a Ctmdp directly from the data returned by @parseNondeterministicModel
+ * @return A Ctmdp Model
+ */
+storm::models::Ctmdp<double> NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile,
+															 std::string const & stateRewardFile, std::string const & transitionRewardFile) {
+	NondeterministicModelParserResultContainer<double> parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+	return storm::models::Ctmdp<double>(parserResult.transitionSystem, parserResult.labeling, parserResult.rowMapping, parserResult.stateRewards, parserResult.transitionRewards);
 }
 
 } /* namespace parser */

src/parser/NondeterministicModelParser.h

@@ -24,40 +24,33 @@ namespace parser {
  *
  *	@note The labeling representation in the file may use at most as much nodes as are specified in the mdp.
  */
-class NondeterministicModelParser: public storm::parser::Parser {
-public:
-	NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
-			std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
 
-	std::shared_ptr<storm::models::Mdp<double>> getMdp() {
-		if (this->mdp == nullptr) {
-			this->mdp = std::shared_ptr<storm::models::Mdp<double>>(new storm::models::Mdp<double>(
-				this->probabilityMatrix, this->stateLabeling, this->rowMapping, this->stateRewards, this->transitionRewardMatrix
-			));
-		}
-		return this->mdp;
-	}
+storm::models::Mdp<double> NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile,
+				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
+storm::models::Ctmdp<double> NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile,
+				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
 
-	std::shared_ptr<storm::models::Ctmdp<double>> getCtmdp() {
-		if (this->ctmdp == nullptr) {
-			this->ctmdp = std::shared_ptr<storm::models::Ctmdp<double>>(new storm::models::Ctmdp<double>(
-				this->probabilityMatrix, this->stateLabeling, this->rowMapping, this->stateRewards, this->transitionRewardMatrix
-			));
-		}
-		return this->ctmdp;
-	}
 
+/*!
+ * @brief This Class acts as a container much like std::pair for the five return values of the NondeterministicModelParser
+ */
+template <class T>
+class NondeterministicModelParserResultContainer {
+public:
+	storm::storage::SparseMatrix<T> transitionSystem;
+	storm::models::AtomicPropositionsLabeling labeling;
+	std::vector<uint_fast64_t> rowMapping;
+	boost::optional<std::vector<T>> stateRewards;
+	boost::optional<storm::storage::SparseMatrix<T>> transitionRewards;
+	NondeterministicModelParserResultContainer(storm::storage::SparseMatrix<T> transitionSystem, std::vector<uint_fast64_t> rowMapping, storm::models::AtomicPropositionsLabeling labeling) : transitionSystem(transitionSystem), rowMapping(rowMapping), labeling(labeling) { }
 private:
-	std::shared_ptr<storm::storage::SparseMatrix<double>> probabilityMatrix;
-	std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
-	std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
-	std::shared_ptr<std::vector<double>> stateRewards;
-	std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewardMatrix;
-
-	std::shared_ptr<storm::models::Mdp<double>> mdp;
-	std::shared_ptr<storm::models::Ctmdp<double>> ctmdp;
+	NondeterministicModelParserResultContainer() {}
 };
 
+
+NondeterministicModelParserResultContainer<double> parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
+				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
+
 } /* namespace parser */
 
 } /* namespace storm */

src/parser/Parser.cpp

@@ -48,6 +48,16 @@ double storm::parser::checked_strtod(const char* str, char** end) {
 	return res;
 }
 
+/*!
+ *  @brief Tests whether the given file exists and is readable.
+ *  @return True iff the file exists and is readable.
+ */
+bool storm::parser::fileExistsAndIsReadable(const char* fileName) {
+	std::ifstream fin(fileName);
+	bool returnValue = !fin.fail();
+	return returnValue;
+}
+
 /*!
  *	Skips spaces, tabs, newlines and carriage returns. Returns pointer
  *	to first char that is not a whitespace.
@@ -59,6 +69,31 @@ char* storm::parser::trimWhitespaces(char* buf) {
 	return buf;
 }
 
+/*!
+ * @briefs Analyzes the given file and tries to find out the used file endings.
+ */
+storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std::string const& fileName) {
+	storm::parser::SupportedLineEndingsEnum result = storm::parser::SupportedLineEndingsEnum::Unsupported;
+
+	MappedFile fileMap(fileName.c_str());
+	char* buf = nullptr;
+	char* const bufferEnd = fileMap.dataend;
+
+	bool sawR = false;
+	for (buf = fileMap.data; buf != bufferEnd; ++buf) {
+		if (*buf == '\r') {
+			// check for following \n
+			if (((buf + sizeof(char)) < bufferEnd) && (*(buf + sizeof(char)) == '\n')) {
+				return storm::parser::SupportedLineEndingsEnum::SlashRN; 
+			}
+			return storm::parser::SupportedLineEndingsEnum::SlashR; 
+		} else if (*buf == '\n') {
+			return storm::parser::SupportedLineEndingsEnum::SlashN;
+		}
+	}
+	return storm::parser::SupportedLineEndingsEnum::Unsupported;
+}
+
 /*!
  *	Will stat the given file, open it and map it to memory.
  *	If anything of this fails, an appropriate exception is raised

src/parser/Parser.h

@@ -17,6 +17,7 @@
 #include <fstream>
 #include <memory>
 #include <vector>
+#include <string>
 
 #include <boost/integer/integer_mask.hpp>
 #include "src/exceptions/FileIoException.h"
@@ -38,25 +39,16 @@ namespace parser {
 			// Intentionally left empty.
 		}
 
-		RewardMatrixInformationStruct(uint_fast64_t rowCount, uint_fast64_t columnCount, std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices)
+		RewardMatrixInformationStruct(uint_fast64_t rowCount, uint_fast64_t columnCount, std::vector<uint_fast64_t> const * const nondeterministicChoiceIndices)
 		: rowCount(rowCount), columnCount(columnCount), nondeterministicChoiceIndices(nondeterministicChoiceIndices) {
 			// Intentionally left empty.
 		}
 
 		uint_fast64_t rowCount;
 		uint_fast64_t columnCount;
-		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices;
+		std::vector<uint_fast64_t> const * const nondeterministicChoiceIndices;
 	};
 
-	/*!
-	 *  @brief Tests whether the given file exists and is readable.
-	 */
-	bool fileExistsAndIsReadable(const char* fileName) {
-		std::ifstream fin(fileName);
-		bool returnValue = !fin.fail();
-		return returnValue;
-	}
-
 	/*!
 	 *	@brief Opens a file and maps it to memory providing a char*
 	 *	containing the file content.
@@ -123,26 +115,41 @@ namespace parser {
 		~MappedFile();
 	};
 
-	class Parser {
-		//protected:
-			
-	};
-
 	/*!
-		*	@brief Parses integer and checks, if something has been parsed.
-		*/
+	 *	@brief Parses integer and checks, if something has been parsed.
+	 */
 	uint_fast64_t checked_strtol(const char* str, char** end);
 
 	/*!
-		*	@brief Parses floating point and checks, if something has been parsed.
-		*/
+	 *	@brief Parses floating point and checks, if something has been parsed.
+	 */
 	double checked_strtod(const char* str, char** end);
 	
 	/*!
-		*	@brief Skips common whitespaces in a string.
-		*/
+	 *	@brief Skips common whitespaces in a string.
+	 */
 	char* trimWhitespaces(char* buf);
 
+	/*!
+	 *  @brief Tests whether the given file exists and is readable.
+	 */
+	bool fileExistsAndIsReadable(const char* fileName);
+
+	/*!
+	 * @brief Enum Class Type containing all supported file endings.
+	 */
+	enum class SupportedLineEndingsEnum : unsigned short {
+		Unsupported = 0,
+		SlashR,
+		SlashN,
+		SlashRN
+	};
+
+	/*!
+	 * @briefs Analyzes the given file and tries to find out the used line endings.
+	 */
+	storm::parser::SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName);
+
 } // namespace parser
 } // namespace storm
 

src/parser/PrctlFileParser.cpp

@@ -13,15 +13,7 @@
 namespace storm {
 namespace parser {
 
-PrctlFileParser::PrctlFileParser() {
-	//Intentionally left empty
-}
-
-PrctlFileParser::~PrctlFileParser() {
-	//intentionally left empty
-}
-
-std::list<storm::property::prctl::AbstractPrctlFormula<double>*> PrctlFileParser::parseFormulas(std::string filename) {
+std::list<storm::property::prctl::AbstractPrctlFormula<double>*> PrctlFileParser(std::string filename) {
 	// Open file
 	std::ifstream inputFileStream(filename, std::ios::in);
 

src/parser/PrctlFileParser.h

@@ -16,34 +16,12 @@ namespace storm {
 namespace parser {
 
 /*!
- * Reads a PRCTL formula from a file and return the formula tree.
+ * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
  *
- * @note
- * This class creates a PctlFormula object which can be accessed through the getFormula() method (of base
- * class PrctlParser). However, it will not delete this object.
+ * @param filename
+ * @return The list of parsed formulas
  */
-class PrctlFileParser {
-public:
-	/*!
-	 * Constructor
-	 */
-	PrctlFileParser();
-
-	/*!
-	 * Destructor.
-	 * At this time, empty
-	 *
-	 */
-	~PrctlFileParser();
-
-	/*!
-	 * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
-	 *
-	 * @param filename
-	 * @return The list of parsed formulas
-	 */
-	std::list<storm::property::prctl::AbstractPrctlFormula<double>*> parseFormulas(std::string filename);
-};
+std::list<storm::property::prctl::AbstractPrctlFormula<double>*> PrctlFileParser(std::string filename);
 
 } /* namespace parser */
 } /* namespace storm */

src/parser/PrctlParser.h

@@ -18,7 +18,7 @@ namespace parser {
  * This class creates a PctlFormula object which can be accessed through the getFormula() method (of base
  * class PrctlParser). However, it will not delete this object.
  */
-class PrctlParser : Parser {
+class PrctlParser {
 	public:
 		/*!
 		 * Reads a PRCTL formula from its string representation and parses it into a formula tree, consisting of

src/parser/PrismParser.cpp

@@ -32,14 +32,14 @@ namespace parser {
  * closes the file properly, even if an exception is thrown in the parser. In this case, the
  * exception is passed on to the caller.
  */
-storm::ir::Program parseFile(std::string const& filename) {
+storm::ir::Program PrismParserFromFile(std::string const& filename) {
 	// Open file and initialize result.
 	std::ifstream inputFileStream(filename, std::ios::in);
 	storm::ir::Program result;
 
 	// Now try to parse the contents of the file.
 	try {
-		result = parse(inputFileStream, filename);
+		result = PrismParser(inputFileStream, filename);
 	} catch(std::exception& e) {
 		// In case of an exception properly close the file before passing exception.
 		inputFileStream.close();
@@ -56,7 +56,7 @@ storm::ir::Program parseFile(std::string const& filename) {
  * If the parser throws an expectation failure exception, i.e. expected input different than the one
  * provided, this is caught and displayed properly before the exception is passed on.
  */
-storm::ir::Program parse(std::istream& inputStream, std::string const& filename) {
+storm::ir::Program PrismParser(std::istream& inputStream, std::string const& filename) {
 	// Prepare iterators to input.
 	// TODO: Right now, this parses the whole contents of the file into a string first.
 	// While this is usually not necessary, because there exist adapters that make an input stream

src/parser/PrismParser.h

@@ -31,7 +31,7 @@ using namespace storm::ir::expressions;
  * @param filename the name of the file to parse.
  * @return a shared pointer to the intermediate representation of the PRISM file.
  */
-storm::ir::Program parseFile(std::string const& filename);
+storm::ir::Program PrismParserFromFile(std::string const& filename);
 
 /*!
  * Parses the given input stream into the intermediate representation assuming it complies with
@@ -40,15 +40,7 @@ storm::ir::Program parseFile(std::string const& filename);
  * @param filename the name of the file the input stream belongs to. Used for diagnostics.
  * @return a shared pointer to the intermediate representation of the PRISM file.
  */
-storm::ir::Program parse(std::istream& inputStream, std::string const& filename);
-
-class PrismParser {
-public:
-	
-	
-private:
-	
-};
+storm::ir::Program PrismParser(std::istream& inputStream, std::string const& filename);
 
 } // namespace parser
 

src/parser/SparseStateRewardParser.cpp

@@ -71,6 +71,7 @@ std::vector<double> SparseStateRewardParser(uint_fast64_t stateCount, std::strin
 			buf = trimWhitespaces(buf);
 		}
 	}
+	return stateRewards;
 }
 
 }  // namespace parser

src/utility/ErrorHandling.h

@@ -24,7 +24,14 @@ std::string demangle(char const* symbol) {
 	char temp[128];
     
 	// Check for C++ symbol, on Non-MSVC Only
-	if (sscanf(symbol, "%*[^(]%*[^_]%127[^)+]", temp) == 1) {
+	int scanResult = 0;
+#ifdef WINDOWS
+	scanResult = sscanf_s(symbol, "%*[^(]%*[^_]%127[^)+]", temp, sizeof(temp));
+#else
+	scanResult = sscanf(symbol, "%*[^(]%*[^_]%127[^)+]", temp);
+#endif
+	
+	if (scanResult == 1) {
 #ifndef WINDOWS
 		char* demangled;
 		if (NULL != (demangled = abi::__cxa_demangle(temp, NULL, NULL, &status))) {
@@ -59,7 +66,13 @@ std::string demangle(char const* symbol) {
 	}
 
 	// Check for C symbol.
-	if (sscanf(symbol, "%127s", temp) == 1) {
+	scanResult = 0;
+#ifdef WINDOWS
+	scanResult = sscanf_s(symbol, "%127s", temp, sizeof(temp));
+#else
+	scanResult = sscanf(symbol, "%127s", temp);
+#endif
+	if (scanResult == 1) {
 		return temp;
 	}
     

test/functional/parser/CslParserTest.cpp

@@ -10,144 +10,130 @@
 #include "src/parser/CslParser.h"
 
 TEST(CslParserTest, parseApOnlyTest) {
-	std::string ap = "ap";
-	storm::parser::CslParser* cslParser = nullptr;
+	std::string formula = "ap";
+	storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
 	ASSERT_NO_THROW(
-			cslParser = new storm::parser::CslParser(ap);
+		cslFormula = storm::parser::CslParser(formula);
 	);
 
-	ASSERT_NE(cslParser->getFormula(), nullptr);
-
-
-	ASSERT_EQ(ap, cslParser->getFormula()->toString());
-
-	delete cslParser->getFormula();
-	delete cslParser;
+	ASSERT_NE(cslFormula, nullptr);
+	ASSERT_EQ(cslFormula->toString(), formula);
 
+	delete cslFormula;
 }
 
 TEST(CslParserTest, parsePropositionalFormulaTest) {
-	storm::parser::CslParser* cslParser = nullptr;
+	std::string formula = "!(a & b) | a & ! c";
+	storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
 	ASSERT_NO_THROW(
-			cslParser = new storm::parser::CslParser("!(a & b) | a & ! c")
+		cslFormula = storm::parser::CslParser(formula);
 	);
 
-	ASSERT_NE(cslParser->getFormula(), nullptr);
-
-
-	ASSERT_EQ(cslParser->getFormula()->toString(), "(!(a & b) | (a & !c))");
-
-	delete cslParser->getFormula();
-	delete cslParser;
+	ASSERT_NE(cslFormula, nullptr);
+	ASSERT_EQ(cslFormula->toString(), "(!(a & b) | (a & !c))");
 
+	delete cslFormula;
 }
 
 TEST(CslParserTest, parseProbabilisticFormulaTest) {
-	storm::parser::CslParser* cslParser = nullptr;
+	std::string formula = "P > 0.5 [ F a ]";
+	storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
 	ASSERT_NO_THROW(
-			cslParser = new storm::parser::CslParser("P > 0.5 [ F a ]")
+		cslFormula = storm::parser::CslParser(formula);
 	);
 
-	ASSERT_NE(cslParser->getFormula(), nullptr);
-
-	storm::property::csl::ProbabilisticBoundOperator<double>* op = static_cast<storm::property::csl::ProbabilisticBoundOperator<double>*>(cslParser->getFormula());
+	ASSERT_NE(cslFormula, nullptr);
 
+	storm::property::csl::ProbabilisticBoundOperator<double>* op = static_cast<storm::property::csl::ProbabilisticBoundOperator<double>*>(cslFormula);
 	ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator());
 	ASSERT_EQ(0.5, op->getBound());
 
-	ASSERT_EQ(cslParser->getFormula()->toString(), "P > 0.500000 [F a]");
-
-	delete cslParser->getFormula();
-	delete cslParser;
+	ASSERT_EQ(cslFormula->toString(), "P > 0.500000 [F a]");
 
+	delete cslFormula;
 }
 
 TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
-	storm::parser::CslParser* cslParser = nullptr;
+	std::string formula = "S >= 15 [ P < 0.2 [ a U<=3 b ] ]";
+	storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
 	ASSERT_NO_THROW(
-			cslParser = new storm::parser::CslParser("S >= 15 [ P < 0.2 [ a U<=3 b ] ]")
+		cslFormula = storm::parser::CslParser(formula);
 	);
 
-	ASSERT_NE(cslParser->getFormula(), nullptr);
-
-	storm::property::csl::SteadyStateBoundOperator<double>* op = static_cast<storm::property::csl::SteadyStateBoundOperator<double>*>(cslParser->getFormula());
+	ASSERT_NE(cslFormula, nullptr);
 
+	storm::property::csl::SteadyStateBoundOperator<double>* op = static_cast<storm::property::csl::SteadyStateBoundOperator<double>*>(cslFormula);
 	ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator());
 	ASSERT_EQ(15.0, op->getBound());
 
-	ASSERT_EQ("S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]", cslParser->getFormula()->toString());
+	ASSERT_EQ(cslFormula->toString(), "S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]");
 
-	delete cslParser->getFormula();
-	delete cslParser;
+	delete cslFormula;
 }
 
 TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) {
-	storm::parser::CslParser* cslParser = nullptr;
+	std::string formula = "S = ? [ P <= 0.5 [ F<=3 a ] ]";
+	storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
 	ASSERT_NO_THROW(
-			cslParser = new storm::parser::CslParser("S = ? [ P <= 0.5 [ F<=3 a ] ]")
+		cslFormula = storm::parser::CslParser(formula);
 	);
 
-	ASSERT_NE(cslParser->getFormula(), nullptr);
+	ASSERT_NE(cslFormula, nullptr);
+	ASSERT_EQ(cslFormula->toString(), "S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]");
 
-
-	ASSERT_EQ(cslParser->getFormula()->toString(), "S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]");
-
-	delete cslParser->getFormula();
-	delete cslParser;
+	delete cslFormula;
 }
 
 TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
-	storm::parser::CslParser* cslParser = nullptr;
+	std::string formula = "P = ? [ a U [3,4] b & (!c) ]";
+	storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
 	ASSERT_NO_THROW(
-			cslParser = new storm::parser::CslParser("P = ? [ a U [3,4] b & (!c) ]")
+		cslFormula = storm::parser::CslParser(formula);
 	);
 
-	ASSERT_NE(cslParser->getFormula(), nullptr);
-
-
-	ASSERT_EQ(cslParser->getFormula()->toString(), "P = ? [a U[3.000000,4.000000] (b & !c)]");
-
-	delete cslParser->getFormula();
-	delete cslParser;
+	ASSERT_NE(cslFormula, nullptr);
+	ASSERT_EQ(cslFormula->toString(), "P = ? [a U[3.000000,4.000000] (b & !c)]");
 
+	delete cslFormula;
 }
 
 
 TEST(CslParserTest, parseComplexFormulaTest) {
-	storm::parser::CslParser* cslParser = nullptr;
+	std::string formula = "S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ])  //and a comment";
+	storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
 	ASSERT_NO_THROW(
-			cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ])  //and a comment")
+		cslFormula = storm::parser::CslParser(formula);
 	);
 
-	ASSERT_NE(cslParser->getFormula(), nullptr);
-
-	ASSERT_EQ("(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F>=7.000000 (a & b)]]))", cslParser->getFormula()->toString());
-	delete cslParser->getFormula();
-	delete cslParser;
+	ASSERT_NE(cslFormula, nullptr);
+	ASSERT_EQ(cslFormula->toString(), "(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F>=7.000000 (a & b)]]))");
 
+	delete cslFormula;
 }
 
 TEST(CslParserTest, wrongProbabilisticFormulaTest) {
-	storm::parser::CslParser* cslParser = nullptr;
-	ASSERT_THROW(cslParser = new storm::parser::CslParser("P > 0.5 [ a ]"),	storm::exceptions::WrongFormatException);
-
-	delete cslParser;
+	std::string formula = "P > 0.5 [ a ]";
+	storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
+	ASSERT_THROW(
+		cslFormula = storm::parser::CslParser(formula),	
+		storm::exceptions::WrongFormatException
+	);
 }
 
 TEST(CslParserTest, wrongFormulaTest) {
-	storm::parser::CslParser* cslParser = nullptr;
+	std::string formula = "(a | b) & +";
+	storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
 	ASSERT_THROW(
-			cslParser = new storm::parser::CslParser("(a | b) & +"),
-			storm::exceptions::WrongFormatException
+		cslFormula = storm::parser::CslParser(formula),	
+		storm::exceptions::WrongFormatException
 	);
-	delete cslParser;
 }
 
 TEST(CslParserTest, wrongFormulaTest2) {
-	storm::parser::CslParser* cslParser = nullptr;
+	std::string formula = "P>0 [ F & a ]";
+	storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
 	ASSERT_THROW(
-			cslParser = new storm::parser::CslParser("P>0 [ F & a ]"),
-			storm::exceptions::WrongFormatException
+		cslFormula = storm::parser::CslParser(formula),	
+		storm::exceptions::WrongFormatException
 	);
-	delete cslParser;
 }

test/functional/parser/LtlParserTest.cpp

@@ -10,34 +10,29 @@
 #include "src/parser/LtlParser.h"
 
 TEST(LtlParserTest, parseApOnlyTest) {
-	std::string ap = "ap";
-	storm::parser::LtlParser* ltlParser = nullptr;
+	std::string formula = "ap";
+	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-			ltlParser = new storm::parser::LtlParser(ap);
+		ltlFormula = storm::parser::LtlParser(formula);
 	);
 
-	ASSERT_NE(ltlParser->getFormula(), nullptr);
+	ASSERT_NE(ltlFormula, nullptr);
+	ASSERT_EQ(ltlFormula->toString(), formula);
 
-
-	ASSERT_EQ(ltlParser->getFormula()->toString(), ap);
-
-	delete ltlParser->getFormula();
-	delete ltlParser;
+	delete ltlFormula;
 }
 
 TEST(LtlParserTest, parsePropositionalFormulaTest) {
-	storm::parser::LtlParser* ltlParser = nullptr;
+	std::string formula = "!(a & b) | a & ! c";
+	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-			ltlParser = new storm::parser::LtlParser("!(a & b) | a & ! c")
+		ltlFormula = storm::parser::LtlParser(formula);
 	);
 
-	ASSERT_NE(ltlParser->getFormula(), nullptr);
-
-
-	ASSERT_EQ(ltlParser->getFormula()->toString(), "(!(a & b) | (a & !c))");
+	ASSERT_NE(ltlFormula, nullptr);
+	ASSERT_EQ(ltlFormula->toString(), "(!(a & b) | (a & !c))");
 
-	delete ltlParser->getFormula();
-	delete ltlParser;
+	delete ltlFormula;
 }
 
 /*!
@@ -45,18 +40,16 @@ TEST(LtlParserTest, parsePropositionalFormulaTest) {
  * "Eventually" operator.
  */
 TEST(LtlParserTest, parseAmbiguousFormulaTest) {
-	storm::parser::LtlParser* ltlParser = nullptr;
+	std::string formula = "F & b";
+	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-			ltlParser = new storm::parser::LtlParser("F & b")
+		ltlFormula = storm::parser::LtlParser(formula);
 	);
 
-	ASSERT_NE(ltlParser->getFormula(), nullptr);
+	ASSERT_NE(ltlFormula, nullptr);
+	ASSERT_EQ(ltlFormula->toString(), "(F & b)");
 
-
-	ASSERT_EQ(ltlParser->getFormula()->toString(), "(F & b)");
-
-	delete ltlParser->getFormula();
-	delete ltlParser;
+	delete ltlFormula;
 }
 
 /*!
@@ -64,89 +57,85 @@ TEST(LtlParserTest, parseAmbiguousFormulaTest) {
  * depending where it occurs.
  */
 TEST(LtlParserTest, parseAmbiguousFormulaTest2) {
-	storm::parser::LtlParser* ltlParser = nullptr;
+	std::string formula = "F F";
+	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-			ltlParser = new storm::parser::LtlParser("F F")
+		ltlFormula = storm::parser::LtlParser(formula);
 	);
 
-	ASSERT_NE(ltlParser->getFormula(), nullptr);
-
+	ASSERT_NE(ltlFormula, nullptr);
+	ASSERT_EQ(ltlFormula->toString(), "F F");
 
-	ASSERT_EQ(ltlParser->getFormula()->toString(), "F F");
-
-	delete ltlParser->getFormula();
-	delete ltlParser;
+	delete ltlFormula;
 }
 
 TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) {
-	storm::parser::LtlParser* ltlParser = nullptr;
+	std::string formula = "F<=5 a";
+	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-			ltlParser = new storm::parser::LtlParser("F<=5 a")
+		ltlFormula = storm::parser::LtlParser(formula);
 	);
 
-	ASSERT_NE(ltlParser->getFormula(), nullptr);
-
-	storm::property::ltl::BoundedEventually<double>* op = static_cast<storm::property::ltl::BoundedEventually<double>*>(ltlParser->getFormula());
+	ASSERT_NE(ltlFormula, nullptr);
 
+	storm::property::ltl::BoundedEventually<double>* op = static_cast<storm::property::ltl::BoundedEventually<double>*>(ltlFormula);
 	ASSERT_EQ(static_cast<uint_fast64_t>(5), op->getBound());
 
-	ASSERT_EQ(ltlParser->getFormula()->toString(), "F<=5 a");
 
-	delete ltlParser->getFormula();
-	delete ltlParser;
+	ASSERT_EQ(ltlFormula->toString(), "F<=5 a");
+
+	delete ltlFormula;
 }
 
 TEST(LtlParserTest, parseBoundedUntilFormulaTest) {
-	storm::parser::LtlParser* ltlParser = nullptr;
+	std::string formula = "a U<=3 b";
+	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-			ltlParser = new storm::parser::LtlParser("a U<=3 b")
+		ltlFormula = storm::parser::LtlParser(formula);
 	);
 
-	ASSERT_NE(ltlParser->getFormula(), nullptr);
-
-	storm::property::ltl::BoundedUntil<double>* op = static_cast<storm::property::ltl::BoundedUntil<double>*>(ltlParser->getFormula());
+	ASSERT_NE(ltlFormula, nullptr);
 
+	storm::property::ltl::BoundedUntil<double>* op = static_cast<storm::property::ltl::BoundedUntil<double>*>(ltlFormula);
 	ASSERT_EQ(static_cast<uint_fast64_t>(3), op->getBound());
 
-	ASSERT_EQ("(a U<=3 b)", ltlParser->getFormula()->toString());
 
-	delete ltlParser->getFormula();
-	delete ltlParser;
+	ASSERT_EQ(ltlFormula->toString(), formula);
+
+	delete ltlFormula;
 }
 
 TEST(LtlParserTest, parseComplexUntilTest) {
-	storm::parser::LtlParser* ltlParser = nullptr;
+	std::string formula = "a U b U<=3 c";
+	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-			ltlParser = new storm::parser::LtlParser("a U b U<=3 c")
+		ltlFormula = storm::parser::LtlParser(formula);
 	);
 
-	ASSERT_NE(ltlParser->getFormula(), nullptr);
-
-
-	ASSERT_EQ(ltlParser->getFormula()->toString(), "((a U b) U<=3 c)");
+	ASSERT_NE(ltlFormula, nullptr);
+	ASSERT_EQ(ltlFormula->toString(), "((a U b) U<=3 c)");
 
-	delete ltlParser->getFormula();
-	delete ltlParser;
+	delete ltlFormula;
 }
 
 TEST(LtlParserTest, parseComplexFormulaTest) {
-	storm::parser::LtlParser* ltlParser = nullptr;
+	std::string formula = "a U F b | G a & F<=3 a U<=7 b // and a comment";
+	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-			ltlParser = new storm::parser::LtlParser("a U F b | G a & F<=3 a U<=7 b //and a comment :P")
+		ltlFormula = storm::parser::LtlParser(formula);
 	);
 
-	ASSERT_NE(ltlParser->getFormula(), nullptr);
+	ASSERT_NE(ltlFormula, nullptr);
+	ASSERT_EQ(ltlFormula->toString(), "(a U F (b | G (a & F<=3 (a U<=7 b))))");
 
-	ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", ltlParser->getFormula()->toString());
-	delete ltlParser->getFormula();
-	delete ltlParser;
+	delete ltlFormula;
 }
 
 TEST(LtlParserTest, wrongFormulaTest) {
-	storm::parser::LtlParser* ltlParser = nullptr;
+	std::string formula = "(a | c) & +";
+	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
 	ASSERT_THROW(
-			ltlParser = new storm::parser::LtlParser("(a | c) & +"),
-			storm::exceptions::WrongFormatException
+		ltlFormula = storm::parser::LtlParser(formula),
+		storm::exceptions::WrongFormatException
 	);
-	delete ltlParser;
 }

test/functional/parser/ParseMdpTest.cpp

@@ -11,21 +11,15 @@
 #include "src/parser/NondeterministicModelParser.h"
 
 TEST(ParseMdpTest, parseAndOutput) {
-	storm::parser::NondeterministicModelParser* mdpParser = nullptr;
-	ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser(
-			STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input_01.tra",
-			STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"));
+	storm::models::Mdp<double> mdp = storm::parser::NondeterministicModelParserAsMdp(
+		STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input_01.tra",
+		STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab");
+	storm::storage::SparseMatrix<double> const& matrix = mdp.getTransitionMatrix();
 
-	std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp();
-	storm::storage::SparseMatrix<double> const& matrix = mdp->getTransitionMatrix();
-
-	ASSERT_EQ(mdp->getNumberOfStates(), (uint_fast64_t)3);
-	ASSERT_EQ(mdp->getNumberOfTransitions(), (uint_fast64_t)11);
+	ASSERT_EQ(mdp.getNumberOfStates(), (uint_fast64_t)3);
+	ASSERT_EQ(mdp.getNumberOfTransitions(), (uint_fast64_t)11);
 	ASSERT_EQ(matrix.getRowCount(), (uint_fast64_t)(2 * 3));
 	ASSERT_EQ(matrix.getColumnCount(), (uint_fast64_t)3);
-	
-
-	delete mdpParser;
 }
 
 

test/functional/parser/ParsePrismTest.cpp

@@ -8,9 +8,8 @@
 #include "src/models/Mdp.h"
 
 TEST(ParsePrismTest, parseCrowds5_5) {
-	storm::parser::PrismParser parser;
 	storm::ir::Program program;
-	ASSERT_NO_THROW(program = parser.parseFile("examples/dtmc/crowds/crowds5_5.pm"));
+	ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile("examples/dtmc/crowds/crowds5_5.pm"));
 	storm::adapters::ExplicitModelAdapter adapter(program);
 
 	std::shared_ptr<storm::models::Dtmc<double>> model = adapter.getModel()->as<storm::models::Dtmc<double>>();
@@ -20,9 +19,8 @@ TEST(ParsePrismTest, parseCrowds5_5) {
 }
 
 TEST(ParsePrismTest, parseTwoDice) {
-	storm::parser::PrismParser parser;
 	storm::ir::Program program;
-	ASSERT_NO_THROW(program = parser.parseFile("examples/mdp/two_dice/two_dice.nm"));
+	ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile("examples/mdp/two_dice/two_dice.nm"));
 	storm::adapters::ExplicitModelAdapter adapter(program);
 
 	std::shared_ptr<storm::models::Mdp<double>> model = adapter.getModel()->as<storm::models::Mdp<double>>();

test/functional/parser/ReadLabFileTest.cpp

@@ -15,77 +15,67 @@
 #include <memory>
 
 TEST(ReadLabFileTest, NonExistingFileTest) {
-   //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
+   // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"!
    ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(0,STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException);
 }
 
 TEST(ReadLabFileTest, ParseTest) {
-	//This test is based on a test case from the original MRMC.
+	// This test is based on a test case from the original MRMC.
 	
-	
-	storm::parser::AtomicPropositionLabelingParser* parser = nullptr;
-	//Parsing the file
-	ASSERT_NO_THROW(parser = new storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"));
-	std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling(parser->getLabeling());
+	// Parsing the file
+	storm::models::AtomicPropositionsLabeling labeling = storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab");
 
-	//Checking whether all propositions are in the labelling
+	// Checking whether all propositions are in the labelling
 
 	char phi[] = "phi", psi[] = "psi", smth[] = "smth";
 
-	if (labeling != nullptr) {
-		ASSERT_TRUE(labeling->containsAtomicProposition(phi));
-		ASSERT_TRUE(labeling->containsAtomicProposition(psi));
-		ASSERT_TRUE(labeling->containsAtomicProposition(smth));
-
-		//Testing whether all and only the correct nodes are labeled with "phi"
-		ASSERT_TRUE(labeling->getStateHasAtomicProposition(phi,0));
-		ASSERT_TRUE(labeling->getStateHasAtomicProposition(phi,1));
-		ASSERT_TRUE(labeling->getStateHasAtomicProposition(phi,2));
-
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,3));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,4));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,5));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,6));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,7));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,8));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,9));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,10));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,11));
-
-		//Testing whether all and only the correct nodes are labeled with "psi"
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,0));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,1));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,2));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,3));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,4));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,5));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,6));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,7));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,8));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,9));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,10));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,11));
-
-		//Testing whether all and only the correct nodes are labeled with "smth"
-		ASSERT_TRUE(labeling->getStateHasAtomicProposition(smth,2));
-
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,0));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,1));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,3));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,4));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,5));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,6));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,7));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,8));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,9));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,10));
-		ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,11));
-
-		//Deleting the labeling
-		delete parser;
-	} else {
-		FAIL();
-	}
+	ASSERT_TRUE(labeling.containsAtomicProposition(phi));
+	ASSERT_TRUE(labeling.containsAtomicProposition(psi));
+	ASSERT_TRUE(labeling.containsAtomicProposition(smth));
+
+	// Testing whether all and only the correct nodes are labeled with "phi"
+	ASSERT_TRUE(labeling.getStateHasAtomicProposition(phi,0));
+	ASSERT_TRUE(labeling.getStateHasAtomicProposition(phi,1));
+	ASSERT_TRUE(labeling.getStateHasAtomicProposition(phi,2));
+
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,3));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,4));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,5));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,6));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,7));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,8));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,9));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,10));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,11));
+
+	//Testing whether all and only the correct nodes are labeled with "psi"
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,0));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,1));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,2));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,3));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,4));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,5));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,6));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,7));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,8));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,9));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,10));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,11));
+
+	//Testing whether all and only the correct nodes are labeled with "smth"
+	ASSERT_TRUE(labeling.getStateHasAtomicProposition(smth,2));
+
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,0));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,1));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,3));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,4));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,5));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,6));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,7));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,8));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,9));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,10));
+	ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,11));
 }
 
 TEST(ReadLabFileTest, WrongHeaderTest1) {

test/functional/parser/ReadTraFileTest.cpp

@@ -17,59 +17,51 @@ TEST(ReadTraFileTest, NonExistingFileTest) {
    ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException);
 }
 
-/* The following test case is based on one of the original STORM test cases
+/* The following test case is based on one of the original MRMC test cases
  */
 TEST(ReadTraFileTest, ParseFileTest1) {
-	storm::parser::DeterministicSparseTransitionParser* parser = nullptr;
-	ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/csl_general_input_01.tra"));
-	std::shared_ptr<storm::storage::SparseMatrix<double>> result = parser->getMatrix();
+	storm::storage::SparseMatrix<double> result = storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/csl_general_input_01.tra");
 
-	if (result != nullptr) {
-		double val = 0;
-		ASSERT_TRUE(result->getValue(0, 0, &val));
-		ASSERT_EQ(val, 0.0);
+	double val = 0.0;
+	ASSERT_TRUE(result.getValue(0, 0, &val));
+	ASSERT_EQ(val, 0.0);
 
-		ASSERT_TRUE(result->getValue(0, 1, &val));
-		ASSERT_EQ(val, 1.0);
+	ASSERT_TRUE(result.getValue(0, 1, &val));
+	ASSERT_EQ(val, 1.0);
 
-		ASSERT_TRUE(result->getValue(1, 1, &val));
-		ASSERT_EQ(val, 0.080645161290322580645161290322581);
+	ASSERT_TRUE(result.getValue(1, 1, &val));
+	ASSERT_EQ(val, 0.080645161290322580645161290322581);
 
-		ASSERT_TRUE(result->getValue(1, 2, &val));
-		ASSERT_EQ(val, 0.080645161290322580645161290322581);
+	ASSERT_TRUE(result.getValue(1, 2, &val));
+	ASSERT_EQ(val, 0.080645161290322580645161290322581);
 
-		//Transition 1->3 was not set in the file, so it is not to appear in the matrix!
-		ASSERT_FALSE(result->getValue(1, 3, &val));
-		ASSERT_EQ(val, 0);
+	//Transition 1->3 was not set in the file, so it is not to appear in the matrix!
+	ASSERT_FALSE(result.getValue(1, 3, &val));
+	ASSERT_EQ(val, 0);
 
-		ASSERT_TRUE(result->getValue(2, 1, &val));
-		ASSERT_EQ(val, 0.04032258064516129032258064516129);
+	ASSERT_TRUE(result.getValue(2, 1, &val));
+	ASSERT_EQ(val, 0.04032258064516129032258064516129);
 
-		ASSERT_TRUE(result->getValue(2, 2, &val));
-		ASSERT_EQ(val, 0.04032258064516129032258064516129);
+	ASSERT_TRUE(result.getValue(2, 2, &val));
+	ASSERT_EQ(val, 0.04032258064516129032258064516129);
 
-		ASSERT_TRUE(result->getValue(2, 3, &val));
-		ASSERT_EQ(val, 0.04032258064516129032258064516129);
+	ASSERT_TRUE(result.getValue(2, 3, &val));
+	ASSERT_EQ(val, 0.04032258064516129032258064516129);
 
-		ASSERT_TRUE(result->getValue(2, 4, &val));
-		ASSERT_EQ(val, 0.04032258064516129032258064516129);
+	ASSERT_TRUE(result.getValue(2, 4, &val));
+	ASSERT_EQ(val, 0.04032258064516129032258064516129);
 
-		ASSERT_TRUE(result->getValue(3, 2, &val));
-		ASSERT_EQ(val, 0.0806451612903225806451612903225812);
+	ASSERT_TRUE(result.getValue(3, 2, &val));
+	ASSERT_EQ(val, 0.0806451612903225806451612903225812);
 
-		ASSERT_TRUE(result->getValue(3, 3, &val));
-		ASSERT_EQ(val, 0.0);
+	ASSERT_TRUE(result.getValue(3, 3, &val));
+	ASSERT_EQ(val, 0.0);
 
-		ASSERT_TRUE(result->getValue(3, 4, &val));
-		ASSERT_EQ(val, 0.080645161290322580645161290322581);
+	ASSERT_TRUE(result.getValue(3, 4, &val));
+	ASSERT_EQ(val, 0.080645161290322580645161290322581);
 
-		ASSERT_TRUE(result->getValue(4, 4, &val));
-		ASSERT_EQ(val, 0.0);
-
-		delete parser;
-	} else {
-		FAIL();
-	}
+	ASSERT_TRUE(result.getValue(4, 4, &val));
+	ASSERT_EQ(val, 0.0);
 }
 
 TEST(ReadTraFileTest, WrongFormatTestHeader1) {