Refactoring on Parser, introduced new keyword "override"

src/formula/Csl/AbstractCslFormula.h

@@ -2,7 +2,7 @@
  * AbstractCslFormula.h
  *
  *  Created on: 19.04.2013
- *      Author: thomas
+ *      Author: Thomas Heinemann
  */
 
 #ifndef ABSTRACTCSLFORMULA_H_
@@ -25,6 +25,13 @@ public:
 	}
 };
 
+/*!
+ * @brief An encapsulation type for the Return Type of the CslParser. As a pure virtual Class can not be an r-value return type, it has to be encapsulated.
+ * @see CslParser
+ */
+template <typename T>
+using AbstractCslFormularRef_t = std::reference_wrapper<storm::property::csl::AbstractCslFormula<T>>;
+
 } /* namespace csl */
 } /* namespace property */
 } /* namespace storm */

src/formula/Ltl/AbstractLtlFormula.h

@@ -82,6 +82,9 @@ public:
 	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const = 0;
 };
 
+template <typename T>
+using AbstractLtlFormularSharedPtr_t = std::shared_ptr<T>;
+
 } /* namespace ltl */
 } /* namespace property */
 } /* namespace storm */

src/parser/AtomicPropositionLabelingParser.cpp

@@ -40,12 +40,15 @@ namespace parser {
  *	@param filename   input .lab file's name.
  *	@return The pointer to the created labeling object.
  */
-AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t node_count,
-		std::string const & filename)
-	: labeling(nullptr) {
+storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const & filename) {
 	/*
 	 *	Open file.
 	 */
+	if (!fileExistsAndIsReadable(filename.c_str())) {
+		LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
+		throw storm::exceptions::WrongFormatException();
+	}
+
 	MappedFile file(filename.c_str());
 	char* buf = file.data;
 
@@ -96,7 +99,7 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
 	/*
 	 *	create labeling object with given node and proposition count
 	 */
-	this->labeling = std::shared_ptr<storm::models::AtomicPropositionsLabeling>(new storm::models::AtomicPropositionsLabeling(node_count, proposition_count));
+	storm::models::AtomicPropositionsLabeling labeling(node_count, proposition_count);
 
 	/*
 	 *	second run: add propositions and node labels to labeling
@@ -130,7 +133,7 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
 				if (strncmp(buf, "#END", cnt) == 0) break;
 				strncpy(proposition, buf, cnt);
 				proposition[cnt] = '\0';
-				this->labeling->addAtomicProposition(proposition);
+				labeling.addAtomicProposition(proposition);
 			} else {
 				cnt = 1;  // next char is separator, one step forward
 			}
@@ -173,13 +176,14 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
 					 */
 					strncpy(proposition, buf, cnt);
 					proposition[cnt] = '\0';
-					this->labeling->addAtomicPropositionToState(proposition, node);
+					labeling.addAtomicPropositionToState(proposition, node);
 					buf += cnt;
 				}
 			}
 			buf = trimWhitespaces(buf);
 		}
 	}
+	return labeling;
 }
 
 }  // namespace parser

src/parser/AtomicPropositionLabelingParser.h

@@ -14,20 +14,8 @@ namespace parser {
 /*!
  *	@brief Load label file and return initialized AtomicPropositionsLabeling object.
  *
- *	Note that this class creates a new AtomicPropositionsLabeling object that can
- *	be accessed via getLabeling(). However, it will not delete this object!
  */
-class AtomicPropositionLabelingParser : Parser {
-	public:
-		AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const &filename);
-
-		std::shared_ptr<storm::models::AtomicPropositionsLabeling> getLabeling() {
-			return this->labeling;
-		}
-
-	private:
-		std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling;
-};
+storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const &filename);
 
 } // namespace parser
 } // namespace storm

src/parser/CslParser.cpp

@@ -38,7 +38,7 @@ namespace storm {
 namespace parser {
 
 template<typename Iterator, typename Skipper>
-struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper > {
+struct CslGrammar : qi::grammar<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper > {
 	CslGrammar() : CslGrammar::base_type(start) {
 		//This block contains helper rules that may be used several times
 		freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))];
@@ -166,7 +166,7 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::Abstr
 
 };
 
-CslParser::CslParser(std::string formulaString) {
+storm::property::csl::AbstractCslFormularRef_t<double> CslParser(std::string formulaString) {
 	// Prepare iterators to input.
 	BaseIteratorType stringIteratorBegin = formulaString.begin();
 	BaseIteratorType stringIteratorEnd = formulaString.end();

src/parser/CslParser.h

@@ -11,14 +11,12 @@
 #include "Parser.h"
 
 #include "src/formula/Csl.h"
-//#include <memory>
+#include <functional>
 
 namespace storm {
 namespace parser {
 
-class CslParser: public storm::parser::Parser {
-public:
-	/*!
+/*!
  * Reads a CSL formula from its string representation and parses it into a formula tree, consisting of
  * classes in the namespace storm::property.
  *
@@ -27,7 +25,17 @@ public:
  * @param formulaString The string representation of the formula
  * @throw wrongFormatException If the input could not be parsed successfully
  */
-	CslParser(std::string formulaString);
+storm::property::csl::AbstractCslFormularRef_t<double> CslParser(std::string formulaString);
+
+/*!
+ * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas.
+ */
+template<typename Iterator, typename Skipper>
+struct CslGrammar;
+
+class CslParser: public storm::parser::Parser {
+public:
+	
 	virtual ~CslParser();
 
 	/*!
@@ -41,11 +49,7 @@ private:
 private:
 	storm::property::csl::AbstractCslFormula<double>* formula;
 
-	/*!
-	 * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas.
-	 */
-	template<typename Iterator, typename Skipper>
-	struct CslGrammar;
+	
 };
 
 } /* namespace parser */

src/parser/DeterministicSparseTransitionParser.cpp

@@ -44,7 +44,7 @@ namespace parser {
  *	@param buf Data to scan. Is expected to be some char array.
  *	@param maxnode Is set to highest id of all nodes.
  */
-uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
+uint_fast64_t firstPass(char* buf, uint_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
 	bool isRewardMatrix = rewardMatrixInformation != nullptr;
 
 	uint_fast64_t nonZeroEntryCount = 0;
@@ -129,8 +129,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas
  *	@return a pointer to the created sparse matrix.
  */
 
-DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation)
-	: matrix(nullptr) {
+storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation) {
 	/*
 	 *	Enforce locale where decimal point is '.'.
 	 */
@@ -138,6 +137,11 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 
 	bool isRewardMatrix = rewardMatrixInformation != nullptr;
 
+	if (!fileExistsAndIsReadable(filename.c_str())) {
+		LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
+		throw storm::exceptions::WrongFormatException();
+	}
+
 	/*
 	 *	Open file.
 	 */
@@ -148,7 +152,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	 *	Perform first pass, i.e. count entries that are not zero.
 	 */
 	uint_fast64_t maxStateId;
-	uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId, rewardMatrixInformation);
+	uint_fast64_t nonZeroEntryCount = firstPass(file.data, maxStateId, rewardMatrixInformation);
 
 	LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros.");
 
@@ -189,12 +193,12 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	 *	The number of non-zero elements is computed by firstPass().
 	 */
 	LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << ".");
-	this->matrix = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(maxStateId + 1));
-	if (this->matrix == nullptr) {
+	storm::storage::SparseMatrix<double> resultMatrix(maxStateId + 1);
+	resultMatrix.initialize(nonZeroEntryCount);
+	if (!resultMatrix.isInitialized()) {
 		LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << ".");
 		throw std::bad_alloc();
 	}
-	this->matrix->initialize(nonZeroEntryCount);
 
 	int_fast64_t row, lastRow = -1, col;
 	double val;
@@ -218,7 +222,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 		if (lastRow != row) {
 			if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
 				if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
-					this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
+					resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
 					LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
 				} else if (!isRewardMatrix) {
 					LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
@@ -229,7 +233,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 			for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
 				hadDeadlocks = true;
 				if (fixDeadlocks && !isRewardMatrix) {
-					this->matrix->addNextValue(skippedRow, skippedRow, storm::utility::constGetOne<double>());
+					resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constGetOne<double>());
 					rowHadDiagonalEntry = true;
 					LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
 				} else if (!isRewardMatrix) {
@@ -246,20 +250,20 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 		} else if (col > row && !rowHadDiagonalEntry) {
 			rowHadDiagonalEntry = true;
 			if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
-				this->matrix->addNextValue(row, row, storm::utility::constGetZero<double>());
+				resultMatrix.addNextValue(row, row, storm::utility::constGetZero<double>());
 				LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
 			} else if (!isRewardMatrix) {
 				LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
 			}
 		}
 
-		this->matrix->addNextValue(row, col, val);
+		resultMatrix.addNextValue(row, col, val);
 		buf = trimWhitespaces(buf);
 	}
 
 	if (!rowHadDiagonalEntry) {
 		if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
-			this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
+			resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
 			LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
 		} else if (!isRewardMatrix) {
 			LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
@@ -271,7 +275,9 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	/*
 	 *	Finalize Matrix.
 	 */	
-	this->matrix->finalize();
+	resultMatrix.finalize();
+
+	return resultMatrix;
 }
 
 }  // namespace parser

src/parser/DeterministicSparseTransitionParser.h

@@ -15,20 +15,7 @@ namespace parser {
  *	@brief	Load a deterministic transition system from file and create a
  *	sparse adjacency matrix whose entries represent the weights of the edges
  */
-class DeterministicSparseTransitionParser : public Parser {
-	public:
-		DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
-
-		std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
-			return this->matrix;
-		}
-
-	private:
-		std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
-
-		uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode, RewardMatrixInformationStruct* rewardMatrixInformation);
-
-};
+storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
 
 } // namespace parser
 } // namespace storm

src/parser/LtlParser.cpp

@@ -41,7 +41,7 @@ namespace storm {
 namespace parser {
 
 template<typename Iterator, typename Skipper>
-struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper > {
+struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper > {
 	LtlGrammar() : LtlGrammar::base_type(start) {
 		//This block contains helper rules that may be used several times
 		freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))];
@@ -128,7 +128,7 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::property::ltl::Abstr
 } //namespace parser
 
 
-storm::parser::LtlParser::LtlParser(std::string formulaString) {
+storm::property::ltl::AbstractLtlFormularSharedPtr_t<double> storm::parser::LtlParser(std::string formulaString) {
 	// Prepare iterators to input.
 	BaseIteratorType stringIteratorBegin = formulaString.begin();
 	BaseIteratorType stringIteratorEnd = formulaString.end();
@@ -178,6 +178,6 @@ storm::parser::LtlParser::LtlParser(std::string formulaString) {
 		throw storm::exceptions::WrongFormatException() << "Syntax error in formula";
 	}
 
-	formula = result_pointer;
+	return storm::property::ltl::AbstractLtlFormularSharedPtr_t<double>(result_pointer);
 }
 

src/parser/LtlParser.h

@@ -14,10 +14,7 @@
 namespace storm {
 namespace parser {
 
-class LtlParser: public storm::parser::Parser {
-public:
-public:
-	/*!
+/*!
 	* Reads a LTL formula from its string representation and parses it into a formula tree, consisting of
 	* classes in the namespace storm::property.
 	*
@@ -26,34 +23,13 @@ public:
 	* @param formulaString The string representation of the formula
 	* @throw wrongFormatException If the input could not be parsed successfully
 	*/
-	LtlParser(std::string formulaString);
+storm::property::ltl::AbstractLtlFormularSharedPtr_t<double> LtlParser(std::string formulaString);
 
-	/*!
-	 *	@return a pointer to the parsed formula object
-	 */
-	storm::property::ltl::AbstractLtlFormula<double>* getFormula() {
-		return this->formula;
-	}
-
-	/*!
-	 * Destructor
-	 *
-	 * Does not delete the parsed formula!
-	 */
-	virtual ~LtlParser() {
-		// Intentionally left empty
-		// The formula is not deleted with the parser.
-	}
-
-private:
-	storm::property::ltl::AbstractLtlFormula<double>* formula;
-
-	/*!
+/*!
  * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas.
  */
-	template<typename Iterator, typename Skipper>
-	struct LtlGrammar;
-};
+template<typename Iterator, typename Skipper>
+struct LtlGrammar;
 
 } /* namespace parser */
 } /* namespace storm */

src/parser/NondeterministicModelParser.cpp

@@ -29,23 +29,21 @@ namespace parser {
  */
 NondeterministicModelParser::NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
 		std::string const & stateRewardFile, std::string const & transitionRewardFile) {
-	storm::parser::NondeterministicSparseTransitionParser tp(transitionSystemFile);
-	uint_fast64_t stateCount = tp.getMatrix()->getColumnCount();
+	NondeterministicSparseTransitionParserResult_t nondeterministicSparseTransitionParserResult = storm::parser::NondeterministicSparseTransitionParser(transitionSystemFile);
+	uint_fast64_t stateCount = nondeterministicSparseTransitionParserResult.first.getColumnCount();
 
-	storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
 	if (stateRewardFile != "") {
-		storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile);
-		this->stateRewards = srp.getStateRewards();
+		std::vector<double> stateRewards = storm::parser::SparseStateRewardParser(stateCount, stateRewardFile);
 	}
 	if (transitionRewardFile != "") {
-		RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(tp.getMatrix()->getRowCount(), tp.getMatrix()->getColumnCount(), tp.getRowMapping());
+		RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(nondeterministicSparseTransitionParserResult.first.getRowCount(), nondeterministicSparseTransitionParserResult.first.getColumnCount(), nondeterministicSparseTransitionParserResult.second);
 		storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, rewardMatrixInfo);
 		delete rewardMatrixInfo;
 		this->transitionRewardMatrix = trp.getMatrix();
 	}
 
 	this->probabilityMatrix = tp.getMatrix();
-	this->stateLabeling = lp.getLabeling();
+	this->stateLabeling = std::shared_ptr<storm::models::AtomicPropositionsLabeling>(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile));
 	this->rowMapping = tp.getRowMapping();
 
 	this->mdp = nullptr;

src/parser/NondeterministicSparseTransitionParser.cpp

@@ -49,7 +49,7 @@ namespace parser {
  *	@param maxnode Is set to highest id of all nodes.
  *	@return The number of non-zero elements.
  */
-uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
+uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
 	bool isRewardFile = rewardMatrixInformation != nullptr;
 
 	/*
@@ -177,13 +177,17 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
  *	@return a pointer to the created sparse matrix.
  */
 
-NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation)
-	: matrix(nullptr) {
+NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation) {
 	/*
 	 *	Enforce locale where decimal point is '.'.
 	 */
 	setlocale(LC_NUMERIC, "C");
 
+	if (!fileExistsAndIsReadable(filename.c_str())) {
+		LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
+		throw storm::exceptions::WrongFormatException();
+	}
+
 	bool isRewardFile = rewardMatrixInformation != nullptr;
 
 	/*
@@ -197,7 +201,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 	 */
 	int_fast64_t maxnode;
 	uint_fast64_t choices;
-	uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode, rewardMatrixInformation);
+	uint_fast64_t nonzero = firstPass(file.data, choices, maxnode, rewardMatrixInformation);
 
 	/*
 	 *	If first pass returned zero, the file format was wrong.
@@ -238,17 +242,18 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 	 *	Those two values, as well as the number of nonzero elements, was been calculated in the first run.
 	 */
 	LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << choices << " x " << (maxnode+1) << " with " << nonzero << " entries.");
-	this->matrix = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(choices, maxnode + 1));
-	if (this->matrix == nullptr) {
+	storm::storage::SparseMatrix<double> matrix(choices, maxnode + 1);
+	matrix.initialize(nonzero);
+	if (!matrix.isInitialized()) {
 		LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << choices << " x " << (maxnode+1) << ".");
 		throw std::bad_alloc();
 	}
-	this->matrix->initialize(nonzero);
+	
 
 	/*
 	 *	Create row mapping.
 	 */
-	this->rowMapping = std::shared_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>(maxnode+2,0));
+	std::vector<uint_fast64_t> rowMapping(maxnode + 2, 0);
 
 	/*
 	 *	Parse file content.
@@ -303,8 +308,8 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 			for (int_fast64_t node = lastsource + 1; node < source; node++) {
 				hadDeadlocks = true;
 				if (fixDeadlocks) {
-					this->rowMapping->at(node) = curRow;
-					this->matrix->addNextValue(curRow, node, 1);
+					rowMapping.at(node) = curRow;
+					matrix.addNextValue(curRow, node, 1);
 					++curRow;
 					LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
 				} else {
@@ -315,14 +320,14 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 				/*
 				 *	Add this source to rowMapping, if this is the first choice we encounter for this state.
 				 */
-				this->rowMapping->at(source) = curRow;
+				rowMapping.at(source) = curRow;
 			}
 		}
 
 		// Read target and value and write it to the matrix.
 		target = checked_strtol(buf, &buf);
 		val = checked_strtod(buf, &buf);
-		this->matrix->addNextValue(curRow, target, val);
+		matrix.addNextValue(curRow, target, val);
 
 		lastsource = source;
 		lastchoice = choice;
@@ -338,7 +343,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 	}
 
 	for (int_fast64_t node = lastsource + 1; node <= maxnode + 1; node++) {
-		this->rowMapping->at(node) = curRow + 1;
+		rowMapping.at(node) = curRow + 1;
 	}
 
 	if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
@@ -346,7 +351,9 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 	/*
 	 * Finalize matrix.
 	 */	
-	this->matrix->finalize();
+	matrix.finalize();
+
+	return std::make_pair(matrix, rowMapping);
 }
 
 }  // namespace parser

src/parser/NondeterministicSparseTransitionParser.h

@@ -13,29 +13,16 @@
 namespace storm {
 namespace parser {
 	
+/*! 
+ * @brief Contains the Result of a call to the NondeterministicSparseTransitionParser function. The first part is the resulting matrix. The second part is the row mapping.
+ */
+typedef std::pair<storm::storage::SparseMatrix<double>, std::vector<uint_fast64_t>> NondeterministicSparseTransitionParserResult_t;
+
 /*!
  *	@brief	Load a nondeterministic transition system from file and create a
  *	sparse adjacency matrix whose entries represent the weights of the edges
  */
-class NondeterministicSparseTransitionParser : public Parser {
-	public:
-		NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
-
-		inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
-			return this->matrix;
-		}
-
-		inline std::shared_ptr<std::vector<uint_fast64_t>> getRowMapping() const {
-			return this->rowMapping;
-		}
-
-	private:
-		std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
-		std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
-
-		uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation);
-
-};
+NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
 
 } // namespace parser
 } // namespace storm

src/parser/Parser.cpp

@@ -20,7 +20,7 @@ extern log4cplus::Logger logger;
  *	@param end New pointer will be written there
  *	@return Result of strtol()
  */
-uint_fast64_t storm::parser::Parser::checked_strtol(const char* str, char** end) {
+uint_fast64_t storm::parser::checked_strtol(const char* str, char** end) {
 	uint_fast64_t res = strtol(str, end, 10);
 	if (str == *end) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing integer. Next input token is not a number.");
@@ -38,7 +38,7 @@ uint_fast64_t storm::parser::Parser::checked_strtol(const char* str, char** end)
  *	@param end New pointer will be written there
  *	@return Result of strtod()
  */
-double storm::parser::Parser::checked_strtod(const char* str, char** end) {
+double storm::parser::checked_strtod(const char* str, char** end) {
 	double res = strtod(str, end);
 	if (str == *end) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing floating point. Next input token is not a number.");
@@ -54,7 +54,7 @@ double storm::parser::Parser::checked_strtod(const char* str, char** end) {
  *	@param buf String buffer
  *	@return	pointer to first non-whitespace character
  */
-char* storm::parser::Parser::trimWhitespaces(char* buf) {
+char* storm::parser::trimWhitespaces(char* buf) {
 	while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++;
 	return buf;
 }

src/parser/Parser.h

@@ -14,6 +14,7 @@
 #include <fcntl.h>
 #include <errno.h>
 #include <iostream>
+#include <fstream>
 #include <memory>
 #include <vector>
 
@@ -47,6 +48,15 @@ namespace parser {
 		std::shared_ptr<std::vector<uint_fast64_t>> 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.
@@ -114,7 +124,10 @@ namespace parser {
 	};
 
 	class Parser {
-		protected:
+		//protected:
+			
+	};
+
 	/*!
 		*	@brief Parses integer and checks, if something has been parsed.
 		*/
@@ -129,7 +142,6 @@ namespace parser {
 		*	@brief Skips common whitespaces in a string.
 		*/
 	char* trimWhitespaces(char* buf);
-	};
 
 } // namespace parser
 } // namespace storm

src/parser/SparseStateRewardParser.cpp

@@ -36,16 +36,20 @@ namespace parser {
  *
  *	@param stateCount The number of states.
  *	@param filename The filename of the state reward file.
- *	@return A pointer to the created state reward vector.
+ *	@return The created state reward vector.
  */
-SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std::string const & filename)
-	: stateRewards(nullptr) {
+std::vector<double> SparseStateRewardParser(uint_fast64_t stateCount, std::string const & filename) {
 	// Open file.
+	if (!fileExistsAndIsReadable(filename.c_str())) {
+		LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
+		throw storm::exceptions::WrongFormatException();
+	}
+
 	MappedFile file(filename.c_str());
 	char* buf = file.data;
 
 	// Create state reward vector with given state count.
-	this->stateRewards = std::shared_ptr<std::vector<double>>(new std::vector<double>(stateCount));
+	std::vector<double> stateRewards(stateCount);
 
 	{
 		// Now parse state reward assignments.
@@ -62,7 +66,7 @@ SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std::
 				throw storm::exceptions::WrongFormatException() << "State reward file specifies illegal reward value.";
 			}
 
-			(*this->stateRewards)[state] = reward;
+			stateRewards[state] = reward;
 
 			buf = trimWhitespaces(buf);
 		}

src/parser/SparseStateRewardParser.h

@@ -13,17 +13,7 @@ namespace parser {
 /*!
  *	@brief Load state reward file and return vector of state rewards.
  */
-class SparseStateRewardParser : Parser {
-	public:
-		SparseStateRewardParser(uint_fast64_t stateCount, std::string const &filename);
-
-		std::shared_ptr<std::vector<double>> getStateRewards() {
-			return this->stateRewards;
-		}
-
-	private:
-		std::shared_ptr<std::vector<double>> stateRewards;
-};
+std::vector<double> SparseStateRewardParser(uint_fast64_t stateCount, std::string const &filename);
 
 } // namespace parser