Reduction of functionality of fileParser: Only does the parsing, no

checking

src/parser/PrctlFileParser.cpp

@@ -16,69 +16,29 @@
 namespace storm {
 namespace parser {
 
-PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Dtmc<double>& dtmc, enum libraries library) {
-	//Here ,the model checker which uses the correct library is created and a reference stored in the pointer modelChecker:
-	storm::modelchecker::SparseDtmcPrctlModelChecker<double>* modelChecker = nullptr;
-	switch(library) {
-	//case EIGEN:
-		//Eigen Model Checker is not completely implemented at the moment, thus using Eigen is not possible...
-		//Current behaviour: Fall back to GMMXX...
-		//modelChecker = new storm::modelchecker::EigenDtmcPrctlModelChecker<double>(dtmc);
-	//	break;
-	case GMMXX:
-	default:					//Note: GMMXX is default, hence default branches here, too.
-		modelChecker = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
-		break;
-	}
-
-	//Now, the check function (which works on abstract model checkers) can parse the formulas and invoke the model checker:
-	check(filename, modelChecker);
-	delete modelChecker;
-}
-
-PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Mdp<double>& mdp, enum libraries library) {
-	//Here ,the model checker which uses the correct library is created and a reference stored in the pointer modelChecker:
-	storm::modelchecker::SparseMdpPrctlModelChecker<double>* modelChecker = nullptr;
-	switch(library) {
-	//case EIGEN:
-		//Eigen MDP Model Checker is not implemented yet
-		//Current behaviour: Fall back to GMMXX...
-	//	break;
-	case GMMXX:
-	default:					//Note: GMMXX is default, hence default branches here, too.
-		modelChecker = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
-		break;
-	}
-
-	//Now, the check function (which works on abstract model checkers) can parse the formulas and invoke the model checker:
-	check(filename, modelChecker);
-	delete modelChecker;
+PrctlFileParser::PrctlFileParser() {
+	//Intentionally left empty
 }
 
 PrctlFileParser::~PrctlFileParser() {
 	//intentionally left empty
 }
 
-void PrctlFileParser::check(std::string filename, storm::modelchecker::AbstractModelChecker<double>* modelChecker) {
+std::list<storm::property::prctl::AbstractPrctlFormula<double>*> parseFormulas(std::string filename) {
 	// Open file
 	std::ifstream inputFileStream(filename, std::ios::in);
+	std::list<storm::property::prctl::AbstractPrctlFormula<double>*> result;
 
 	while(!inputFileStream.eof()) {
 		std::string line;
 		//The while loop reads the input file line by line
 		while (std::getline(inputFileStream, line)) {
 			PrctlParser parser(line);
-			storm::property::prctl::AbstractStateFormula<double>* stateFormula = dynamic_cast<storm::property::prctl::AbstractStateFormula<double>*>(parser.getFormula());
-			if (stateFormula != nullptr) {
-				modelChecker->check(*stateFormula);
-			}
-			storm::property::prctl::AbstractNoBoundOperator<double>* noBoundFormula = dynamic_cast<storm::property::prctl::AbstractNoBoundOperator<double>*>(parser.getFormula());
-			if (noBoundFormula != nullptr) {
-				modelChecker->check(*noBoundFormula);
-			}
-			delete parser.getFormula();
+			result.push_back(parser.getFormula());
 		}
 	}
+
+	return result;
 }
 
 } /* namespace parser */

src/parser/PrctlFileParser.h

@@ -8,10 +8,9 @@
 #ifndef STORM_PARSER_PRCTLFILEPARSER_H_
 #define STORM_PARSER_PRCTLFILEPARSER_H_
 
-#include "models/Dtmc.h"
-#include "models/Mdp.h"
 #include "formula/Prctl.h"
-#include "modelchecker/AbstractModelChecker.h"
+
+#include <list>
 
 namespace storm {
 namespace parser {
@@ -25,46 +24,25 @@ namespace parser {
  */
 class PrctlFileParser {
 public:
-	enum libraries {
-		GMMXX,
-		EIGEN
-	};
-
 	/*!
-	 * Reads a given file of formulas and checks each of these against a given DTMC.
-	 *
-	 * @param filename The name of the file to parse
-	 * @param dtmc		 The DTMC model to check
-	 * @param library  Specifies the library that should perform the algebraic operations during model checking (default is GMMxx)
-	 */
-	PrctlFileParser(std::string filename, storm::models::Dtmc<double>& dtmc, enum libraries library=GMMXX);
-
-	/*!
-	 * Reads a given file of formulas and checks each of these against a given MDP.
-	 *
-	 * @param filename The name of the file to parse
-	 * @param mdp		 The MDP model to check
-	 * @param library  Specifies the library that should perform the algebraic operations during model checking (default is GMMxx, which at the moment also is the only implemented version...)
+	 * Constructor
 	 */
-	PrctlFileParser(std::string filename, storm::models::Mdp<double>& mdp, enum libraries library=GMMXX);
+	PrctlFileParser();
 
-protected:
 	/*!
-	 * Does the actual checking.
-	 * This procedure is equal for all model types (only the model checker is different, so it has to be created in
-	 * different methods beforehand)
+	 * Destructor.
+	 * At this time, empty
 	 *
-	 * @param filename     The name of the file to parse
-	 * @param modelChecker The model checker that checks the formula (has to know its model!)
 	 */
-	void check(std::string filename, storm::modelchecker::AbstractModelChecker<double>* modelChecker);
+	virtual ~PrctlFileParser();
 
 	/*!
-	 * Destructor.
-	 * At this time, empty
+	 * 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
 	 */
-	virtual ~PrctlFileParser();
+	std::list<storm::property::prctl::AbstractPrctlFormula<double>*> parseFormulas(std::string filename);
 };
 
 } /* namespace parser */