Refactored the DeterministicModelParser.

Former-commit-id: 7227d25499

.gitignore

@@ -39,3 +39,6 @@ build//CMakeLists.txt
 /*.vcxproj
 /*.filters
 /*.sln
+#Temp texteditor files
+*.orig
+*.*~

src/parser/AutoParser.h

@@ -48,11 +48,11 @@ class AutoParser {
 			// Do actual parsing
 			switch (type) {
 				case storm::models::DTMC: {
-					this->model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParserAsDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
+					this->model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParser::parseDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
 					break;
 				}
 				case storm::models::CTMC: {
-					this->model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParserAsCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
+					this->model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParser::parseCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
 					break;
 				}
 				case storm::models::MDP: {

src/parser/DeterministicModelParser.cpp

@@ -26,8 +26,7 @@ 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)
  */
-DeterministicModelParserResultContainer<double> parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
-																		std::string const & stateRewardFile, std::string const & transitionRewardFile) {
+DeterministicModelParser::ResultContainer DeterministicModelParser::parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
 
 	storm::storage::SparseMatrix<double> resultTransitionSystem(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionSystemFile)));
 
@@ -36,11 +35,14 @@ DeterministicModelParserResultContainer<double> parseDeterministicModel(std::str
 
 	storm::models::AtomicPropositionsLabeling resultLabeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)));
 
-	DeterministicModelParserResultContainer<double> result(std::move(resultTransitionSystem), std::move(resultLabeling));
+	DeterministicModelParser::ResultContainer result(std::move(resultTransitionSystem), std::move(resultLabeling));
 
+	// Only parse state rewards of a file is given.
 	if (stateRewardFile != "") {
 		result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile));
 	}
+
+	// Only parse transition rewards of a file is given.
 	if (transitionRewardFile != "") {
 		RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, nullptr);
 		result.transitionRewards.reset(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo)));
@@ -50,24 +52,24 @@ DeterministicModelParserResultContainer<double> parseDeterministicModel(std::str
 }
 
 /*!
- * 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
+ * Uses the parseDeterministicModel function 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(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
+storm::models::Dtmc<double> DeterministicModelParser::parseDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
+
+	DeterministicModelParser::ResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
 	return storm::models::Dtmc<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
 }
 
 /*!
- * 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
+ * Uses the parseDeterministicModel function 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(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
+storm::models::Ctmc<double> DeterministicModelParser::parseCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
+
+	DeterministicModelParser::ResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
 	return storm::models::Ctmc<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
 }
 

src/parser/DeterministicModelParser.h

@@ -18,44 +18,77 @@ namespace storm {
 namespace parser {
 
 /*!
- *	@brief Load label and transition file and returns an initialized dtmc or ctmc object.
+ *	@brief Loads a deterministic model (Dtmc or Ctmc) from files.
+ *
+ *	Given the file paths of the files holding the transitions, the atomic propositions and optionally the state- and transition rewards
+ *	it loads the files, parses them and returns the desired model.
  *
  *	@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 {
 
-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 = "");
+public:
 
-/*!
- * @brief This Class acts as a container much like std::pair for the four return values of the DeterministicModelParser
+	/*!
+	 * @brief A struct containing the parsed components of a deterministic model.
 	 */
-template <class T>
-class DeterministicModelParserResultContainer {
-public:
-	storm::storage::SparseMatrix<T> transitionSystem;
+	struct ResultContainer {
+
+		ResultContainer(storm::storage::SparseMatrix<double>& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) {
+			// Intentionally left empty.
+		}
+
+		ResultContainer(storm::storage::SparseMatrix<double>&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) {
+			// Intentionally left empty.
+		}
+
+		// A matrix representing the transitions of the model
+		storm::storage::SparseMatrix<double> transitionSystem;
+
+		// The labels of each state.
 		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) { }
-	DeterministicModelParserResultContainer(storm::storage::SparseMatrix<T>&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) { }
-
-	DeterministicModelParserResultContainer(const DeterministicModelParserResultContainer & other) : transitionSystem(other.transitionSystem), 
-		labeling(other.labeling), stateRewards(other.stateRewards), transitionRewards(other.transitionRewards) {}
-	DeterministicModelParserResultContainer(DeterministicModelParserResultContainer && other) : transitionSystem(std::move(other.transitionSystem)), 
-		labeling(std::move(other.labeling)), stateRewards(std::move(other.stateRewards)), transitionRewards(std::move(other.transitionRewards)) {}
+
+		// Optional rewards for each state.
+		boost::optional<std::vector<double>> stateRewards;
+
+		// Optional rewards for each transition.
+		boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
+	};
+
+
+	/*!
+	 * @brief Parse a Dtmc.
+	 */
+	static storm::models::Dtmc<double> parseDtmc(std::string const & transitionSystemFile,
+												 std::string const & labelingFile,
+												 std::string const & stateRewardFile = "",
+												 std::string const & transitionRewardFile = "");
+
+	/*!
+	 * @brief Parse a Ctmc.
+	 */
+	static storm::models::Ctmc<double> parseCtmc(std::string const & transitionSystemFile,
+										  	     std::string const & labelingFile,
+										  	     std::string const & stateRewardFile = "",
+										  	     std::string const & transitionRewardFile = "");
+
 private:
-	DeterministicModelParserResultContainer() {}
-};
 
+	/*!
+	 * @brief Call sub-parsers on the given files and fill the container with the results.
+	 */
+	static ResultContainer parseDeterministicModel(std::string const & transitionSystemFile,
+												   std::string const & labelingFile,
+												   std::string const & stateRewardFile = "",
+												   std::string const & transitionRewardFile = "");
 
-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/DeterministicSparseTransitionParser.cpp

@@ -7,22 +7,15 @@
 
 #include "src/parser/DeterministicSparseTransitionParser.h"
 
-#include <errno.h>
-#include <time.h>
-#include <sys/stat.h>
-#include <fcntl.h>
-#include <locale.h>
-
-#include <cstdlib>
 #include <cstdio>
 #include <cstring>
+#include <cstdint>
 #include <clocale>
 #include <iostream>
 #include <string>
 
 #include "src/exceptions/FileIoException.h"
 #include "src/exceptions/WrongFormatException.h"
-#include <cstdint>
 #include "src/settings/Settings.h"
 
 #include "log4cplus/logger.h"

src/parser/DeterministicSparseTransitionParser.h

@@ -2,11 +2,7 @@
 #define STORM_PARSER_TRAPARSER_H_
 
 #include "src/storage/SparseMatrix.h"
-
 #include "src/parser/Parser.h"
-#include "src/utility/OsDetection.h"
-
-#include <memory>
 
 namespace storm {
 

src/parser/MarkovAutomatonParser.cpp

@@ -1,6 +1,7 @@
 #include "MarkovAutomatonParser.h"
 #include "AtomicPropositionLabelingParser.h"
 #include "SparseStateRewardParser.h"
+#include "src/exceptions/WrongFormatException.h"
 
 namespace storm {
 

src/parser/MarkovAutomatonSparseTransitionParser.cpp

@@ -1,6 +1,7 @@
 #include "MarkovAutomatonSparseTransitionParser.h"
 
 #include "src/settings/Settings.h"
+#include "src/exceptions/WrongFormatException.h"
 
 namespace storm {
 
@@ -18,8 +19,8 @@ MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTran
 	}
 
 	// Now read the transitions.
-	int_fast64_t source, target = -1;
-	int_fast64_t lastsource = -1;
+	uint_fast64_t source, target = 0;
+	uint_fast64_t lastsource = 0;
 	bool encounteredEOF = false;
 	bool stateHasMarkovianChoice = false;
 	bool stateHasProbabilisticChoice = false;
@@ -150,8 +151,8 @@ MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitio
 	buf = storm::parser::forwardToNextLine(buf, lineEndings);
 
 	// Now read the transitions.
-	int_fast64_t source, target = -1;
-	int_fast64_t lastsource = -1;
+	uint_fast64_t source, target = 0;
+	uint_fast64_t lastsource = 0;
 	bool encounteredEOF = false;
 	uint_fast64_t currentChoice = 0;
 	while (buf[0] != '\0' && !encounteredEOF) {

src/parser/Parser.cpp

@@ -1,10 +1,13 @@
 #include "src/parser/Parser.h"
 
+#include <fcntl.h>
 #include <iostream>
+#include <fstream>
 #include <cstring>
 #include <string>
 #include <cerrno>
 
+#include <boost/integer/integer_mask.hpp>
 #include "src/exceptions/FileIoException.h"
 #include "src/exceptions/WrongFormatException.h"
 #include "src/utility/OsDetection.h"

src/parser/Parser.h

@@ -11,18 +11,9 @@
 #include "src/utility/OsDetection.h"
 
 #include <sys/stat.h>
-#include <fcntl.h>
-#include <errno.h>
-#include <iostream>
-#include <fstream>
-#include <memory>
 #include <vector>
 #include <string>
 
-#include <boost/integer/integer_mask.hpp>
-#include "src/exceptions/FileIoException.h"
-#include "src/exceptions/WrongFormatException.h"
-
 namespace storm {
 
 /*!

test/functional/parser/CslParserTest.cpp

@@ -8,6 +8,7 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 #include "src/parser/CslParser.h"
+#include "src/exceptions/WrongFormatException.h"
 
 TEST(CslParserTest, parseApOnlyTest) {
 	std::string formula = "ap";

test/functional/parser/LtlParserTest.cpp

@@ -8,6 +8,7 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 #include "src/parser/LtlParser.h"
+#include "src/exceptions/WrongFormatException.h"
 
 TEST(LtlParserTest, parseApOnlyTest) {
 	std::string formula = "ap";

test/functional/parser/PrctlParserTest.cpp

@@ -9,6 +9,7 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 #include "src/parser/PrctlParser.h"
+#include "src/exceptions/WrongFormatException.h"
 
 TEST(PrctlParserTest, parseApOnlyTest) {
 	std::string ap = "ap";