Edited Parsers, re factored interface into a single function without an encapsulating class. Warning, this is work in Progress and not yet compiling.

src/exceptions/InvalidStateException.h

@@ -8,7 +8,7 @@ namespace storm {
 namespace exceptions {
 
 /*! 
- * @brief This exception is thrown when a memory request can't be
+ * @brief This exception is thrown when a memory request can not be
  * fulfilled.
  */
 STORM_EXCEPTION_DEFINE_NEW(InvalidStateException)

src/models/AbstractDeterministicModel.h

@@ -32,6 +32,19 @@ class AbstractDeterministicModel: public AbstractModel<T> {
 			: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) {
 		}
 
+		/*! Constructs an abstract 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 stateRewardVector The reward values associated with the states.
+		 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
+		 */
+		AbstractDeterministicModel(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
+				boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix)
+			: AbstractModel<T>(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) {
+		}
+
 		/*!
 		 * Destructor.
 		 */

src/models/AbstractModel.h

@@ -8,6 +8,8 @@
 #include <memory>
 #include <vector>
 
+#include <boost/optional.hpp>
+
 namespace storm {
 namespace models {
 
@@ -48,6 +50,31 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 			// Intentionally left empty.
 		}
 
+		/*! Constructs an abstract model from the given transition matrix and
+		 * the given labeling of the states. Creates copies of all given references.
+		 * @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 stateRewardVector The reward values associated with the states.
+		 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
+		 */
+		AbstractModel(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
+				boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix) {
+			this->transitionMatrix.reset(new storm::storage::SparseMatrix<T>(transitionMatrix));
+			this->stateLabeling.reset(new storm::models::AtomicPropositionsLabeling(stateLabeling));
+					
+			this->stateRewardVector = nullptr;
+			this->transitionRewardMatrix = nullptr;
+
+			if (optionalStateRewardVector) { // Boost::Optional
+				this->stateRewardVector.reset(new std::vector<T>(optionalStateRewardVector.get()));
+			}
+
+			if (optionalTransitionRewardMatrix) { // Boost::Optional
+				this->stateRewardVector.reset(new storm::storage::SparseMatrix<T>(optionalTransitionRewardMatrix.get()));
+			}
+		}
+
 		/*!
 		 * Destructor.
 		 */

src/models/Ctmc.h

@@ -43,6 +43,19 @@ public:
 			: AbstractDeterministicModel<T>(rateMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) {
 	}
 
+	/*!
+	 * Constructs a CTMC object from the given transition rate matrix and
+	 * the given labeling of the states.
+	 * @param rateMatrix The transition rate function of the
+	 * CTMC given by a matrix.
+	 * @param stateLabeling The labeling that assigns a set of atomic
+	 * propositions to each state.
+	 */
+	Ctmc(storm::storage::SparseMatrix<T> const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
+				boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix)
+			: AbstractDeterministicModel<T>(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) {
+	}
+
 	//! Copy Constructor
 	/*!
 	 * Copy Constructor. Performs a deep copy of the given CTMC.

src/models/Dtmc.h

@@ -57,6 +57,31 @@ public:
 		}
 	}
 
+	/*!
+	 * Constructs a DTMC object from the given transition probability matrix and
+	 * the given labeling of the states.
+	 * All values are copied.
+	 * @param probabilityMatrix The matrix representing the transitions in the model.
+	 * @param stateLabeling The labeling that assigns a set of atomic
+	 * propositions to each state.
+	 * @param stateRewardVector The reward values associated with the states.
+	 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
+	 */
+	Dtmc(storm::storage::SparseMatrix<T> const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
+				boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix)
+			: AbstractDeterministicModel<T>(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) {
+		if (!this->checkValidityOfProbabilityMatrix()) {
+			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())) {
+				LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
+				throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions.";
+			}
+		}
+	}
+
 	//! Copy Constructor
 	/*!
 	 * Copy Constructor. Performs a deep copy of the given DTMC.

src/parser/CslParser.cpp

@@ -166,7 +166,7 @@ struct CslGrammar : qi::grammar<Iterator, storm::property::csl::AbstractCslFormu
 
 };
 
-storm::property::csl::AbstractCslFormularRef_t<double> CslParser(std::string formulaString) {
+storm::property::csl::AbstractCslFormula<double>* CslParser(std::string formulaString) {
 	// Prepare iterators to input.
 	BaseIteratorType stringIteratorBegin = formulaString.begin();
 	BaseIteratorType stringIteratorEnd = formulaString.end();
@@ -216,12 +216,7 @@ storm::property::csl::AbstractCslFormularRef_t<double> CslParser(std::string for
 		throw storm::exceptions::WrongFormatException() << "Syntax error in formula";
 	}
 
-	formula = result_pointer;
-}
-
-CslParser::~CslParser() {
-	// Intentionally left empty
-	// Parsed formula is not deleted with the parser!
+	return result_pointer;
 }
 
 } /* namespace parser */

src/parser/CslParser.h

@@ -25,7 +25,7 @@ namespace parser {
  * @param formulaString The string representation of the formula
  * @throw wrongFormatException If the input could not be parsed successfully
  */
-storm::property::csl::AbstractCslFormularRef_t<double> CslParser(std::string formulaString);
+storm::property::csl::AbstractCslFormula<double>* CslParser(std::string formulaString);
 
 /*!
  * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas.
@@ -33,25 +33,6 @@ storm::property::csl::AbstractCslFormularRef_t<double> CslParser(std::string for
 template<typename Iterator, typename Skipper>
 struct CslGrammar;
 
-class CslParser: public storm::parser::Parser {
-public:
-	
-	virtual ~CslParser();
-
-	/*!
-	 *	@return a pointer to the parsed formula object
-	 */
-	storm::property::csl::AbstractCslFormula<double>* getFormula() {
-		return this->formula;
-	}
-
-private:
-private:
-	storm::property::csl::AbstractCslFormula<double>* formula;
-
-	
-};
-
 } /* namespace parser */
 } /* namespace storm */
 #endif /* STORM_PARSER_CSLPARSER_H_ */

src/parser/DeterministicModelParser.cpp

@@ -18,8 +18,7 @@ namespace storm {
 namespace parser {
 
 /*!
- * Parses a transition file and a labeling file and produces a DTMC out of them; a pointer to the dtmc
- * is saved in the field "dtmc"
+ * Parses a transition file and a labeling file
  * 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,31 +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)
  */
-DeterministicModelParser::DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
-		std::string const & stateRewardFile, std::string const & transitionRewardFile) {
-	storm::parser::DeterministicSparseTransitionParser tp(transitionSystemFile);
-	this->transitionSystem = tp.getMatrix();
+DeterministicModelParserResultContainer<double> parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
+																		std::string const & stateRewardFile, std::string const & transitionRewardFile) {
 
-	uint_fast64_t stateCount = this->transitionSystem->getRowCount();
+	storm::storage::SparseMatrix<double> resultTransitionSystem = storm::parser::DeterministicSparseTransitionParser(transitionSystemFile);
 
-	storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
-	this->labeling = lp.getLabeling();
+	uint_fast64_t stateCount = resultTransitionSystem.getRowCount();
 
-	this->stateRewards = nullptr;
-	this->transitionRewards = nullptr;
+	storm::models::AtomicPropositionsLabeling resultLabeling = storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile);
+
+	DeterministicModelParserResultContainer<double> result(resultTransitionSystem, resultLabeling);
 
 	if (stateRewardFile != "") {
-		storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile);
-		this->stateRewards = srp.getStateRewards();
+		result.stateRewards.reset(storm::parser::SparseStateRewardParser(stateCount, stateRewardFile));
 	}
 	if (transitionRewardFile != "") {
 		RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(stateCount, stateCount, nullptr);
-		storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile, false, rewardMatrixInfo);
+		result.transitionRewards.reset(storm::parser::DeterministicSparseTransitionParser(transitionRewardFile, false, rewardMatrixInfo));
 		delete rewardMatrixInfo;
-		this->transitionRewards = trp.getMatrix();
 	}
-	this->dtmc = nullptr;
-	this->ctmc = nullptr;
+
+	return result;
+}
+
+/*!
+ * Uses the Function parseDeterministicModel internally to parse the given input files.
+ * @note This is a Short-Hand for Constructing a Dtmc directly from the data returned by @parseDeterministicModel
+ * @return A Dtmc Model
+ */
+storm::models::Dtmc<double> DeterministicModelParserAsDtmc(std::string const & transitionSystemFile, std::string const & labelingFile,
+														   std::string const & stateRewardFile, std::string const & transitionRewardFile) {
+	DeterministicModelParserResultContainer<double> parserResult = parseDeterministicModel(transitionRewardFile, labelingFile, stateRewardFile, transitionRewardFile);
+	return storm::models::Dtmc<double>(parserResult.transitionSystem, parserResult.labeling, parserResult.stateRewards, parserResult.transitionRewards);
+}
+
+/*!
+ * Uses the Function parseDeterministicModel internally to parse the given input files.
+ * @note This is a Short-Hand for Constructing a Ctmc directly from the data returned by @parseDeterministicModel
+ * @return A Ctmc Model
+ */
+storm::models::Ctmc<double> DeterministicModelParserAsCtmc(std::string const & transitionSystemFile, std::string const & labelingFile,
+				std::string const & stateRewardFile, std::string const & transitionRewardFile) {
+	DeterministicModelParserResultContainer<double> parserResult = parseDeterministicModel(transitionRewardFile, labelingFile, stateRewardFile, transitionRewardFile);
+	return storm::models::Ctmc<double>(parserResult.transitionSystem, parserResult.labeling, parserResult.stateRewards, parserResult.transitionRewards);
 }
 
 } /* namespace parser */

src/parser/DeterministicModelParser.h

@@ -12,51 +12,44 @@
 #include "src/models/Dtmc.h"
 #include "src/models/Ctmc.h"
 
+#include <boost/optional.hpp>
+
 namespace storm {
 namespace parser {
 
 /*!
- *	@brief Load label and transition file and return initialized dtmc or ctmc object.
+ *	@brief Load label and transition file and returns an initialized dtmc or ctmc object.
  *
- *	@note This class creates a new Dtmc or Ctmc object that can
- *	be accessed via getDtmc() or getCtmc(). However, it will not delete this object!
+ *	@note This class creates a new Dtmc or Ctmc object
  *
  *	@note The labeling representation in the file may use at most as much nodes as are specified in the transition system.
  */
-class DeterministicModelParser: public storm::parser::Parser {
-	public:
-		DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+
+
+storm::models::Dtmc<double> DeterministicModelParserAsDtmc(std::string const & transitionSystemFile, std::string const & labelingFile,
+				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
+storm::models::Ctmc<double> DeterministicModelParserAsCtmc(std::string const & transitionSystemFile, std::string const & labelingFile,
 				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
 
-		/*!
-		 *	@brief	Get the parsed dtmc model.
-		 */
-		std::shared_ptr<storm::models::Dtmc<double>> getDtmc() {
-			if (this->dtmc == nullptr) {
-				this->dtmc = std::shared_ptr<storm::models::Dtmc<double>>(new storm::models::Dtmc<double>(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards));
-			}
-			return this->dtmc;
-		}
-		/*!
-		 *	@brief	Get the parsed ctmc model.
-		 */
-		std::shared_ptr<storm::models::Ctmc<double>> getCtmc() {
-			if (this->ctmc == nullptr) {
-				this->ctmc = std::shared_ptr<storm::models::Ctmc<double>>(new storm::models::Ctmc<double>(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards));
-			}
-			return this->ctmc;
-		}
-
-	private:
-		std::shared_ptr<storm::storage::SparseMatrix<double>> transitionSystem;
-		std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling;
-		std::shared_ptr<std::vector<double>> stateRewards;
-		std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards;
-
-		std::shared_ptr<storm::models::Dtmc<double>> dtmc;
-		std::shared_ptr<storm::models::Ctmc<double>> ctmc;
+/*!
+ * @brief This Class acts as a container much like std::pair for the four return values of the DeterministicModelParser
+ */
+template <class T>
+class DeterministicModelParserResultContainer {
+public:
+	storm::storage::SparseMatrix<T> transitionSystem;
+	storm::models::AtomicPropositionsLabeling labeling;
+	boost::optional<std::vector<T>> stateRewards;
+	boost::optional<storm::storage::SparseMatrix<T>> transitionRewards;
+	DeterministicModelParserResultContainer(storm::storage::SparseMatrix<T>& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { }
+private:
+	DeterministicModelParserResultContainer() {}
 };
 
+
+DeterministicModelParserResultContainer<double> parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
+				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
+
 } /* namespace parser */
 } /* namespace storm */
 #endif /* STORM_PARSER_DETERMINISTICMODELPARSER_H_ */

src/parser/LtlParser.cpp

@@ -128,7 +128,7 @@ struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormu
 } //namespace parser
 
 
-storm::property::ltl::AbstractLtlFormularSharedPtr_t<double> storm::parser::LtlParser(std::string formulaString) {
+storm::property::ltl::AbstractLtlFormula<double>* storm::parser::LtlParser(std::string formulaString) {
 	// Prepare iterators to input.
 	BaseIteratorType stringIteratorBegin = formulaString.begin();
 	BaseIteratorType stringIteratorEnd = formulaString.end();
@@ -178,6 +178,6 @@ storm::property::ltl::AbstractLtlFormularSharedPtr_t<double> storm::parser::LtlP
 		throw storm::exceptions::WrongFormatException() << "Syntax error in formula";
 	}
 
-	return storm::property::ltl::AbstractLtlFormularSharedPtr_t<double>(result_pointer);
+	return result_pointer;
 }
 

src/parser/LtlParser.h

@@ -23,7 +23,7 @@ namespace parser {
 	* @param formulaString The string representation of the formula
 	* @throw wrongFormatException If the input could not be parsed successfully
 	*/
-storm::property::ltl::AbstractLtlFormularSharedPtr_t<double> LtlParser(std::string formulaString);
+storm::property::ltl::AbstractLtlFormula<double>* LtlParser(std::string formulaString);
 
 /*!
  * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas.

src/parser/PrismParser.cpp

@@ -32,7 +32,7 @@ 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 PrismParser::parseFile(std::string const& filename) const {
+storm::ir::Program parseFile(std::string const& filename) {
 	// Open file and initialize result.
 	std::ifstream inputFileStream(filename, std::ios::in);
 	storm::ir::Program result;
@@ -56,7 +56,7 @@ storm::ir::Program PrismParser::parseFile(std::string const& filename) const {
  * 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 PrismParser::parse(std::istream& inputStream, std::string const& filename) const {
+storm::ir::Program parse(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

@@ -21,28 +21,33 @@ namespace parser {
 using namespace storm::ir;
 using namespace storm::ir::expressions;
 
+/*
+ * This functions parse the format of the PRISM model checker into an intermediate representation.
+ */
+
+/*!
+ * Parses the given file into the intermediate representation assuming it complies with the
+ * PRISM syntax.
+ * @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);
+
 /*!
- * This class parses the format of the PRISM model checker into an intermediate representation.
+ * Parses the given input stream into the intermediate representation assuming it complies with
+ * the PRISM syntax.
+ * @param inputStream the input stream to parse.
+ * @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:
-	/*!
-	 * Parses the given file into the intermediate representation assuming it complies with the
-	 * PRISM syntax.
-	 * @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) const;
+	
 	
 private:
-	/*!
-	 * Parses the given input stream into the intermediate representation assuming it complies with
-	 * the PRISM syntax.
-	 * @param inputStream the input stream to parse.
-	 * @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) const;
+	
 };
 
 } // namespace parser