Start of implementing improved file parser for formulas

src/modelchecker/AbstractModelChecker.h

@@ -111,6 +111,13 @@ public:
 		return result;
 	}
 
+	/*!
+	 * Checks the given state formula on the DTMC and prints the result (true/false) for all initial
+	 * states. (Abstract)
+	 * @param stateFormula The formula to be checked.
+	 */
+	virtual void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const = 0;
+
 	/*!
 	 * The check method for a state formula with a bound operator node as root in
 	 * its formula tree

src/parser/PrctlFileParser.cpp

@@ -7,10 +7,12 @@
 
 #include "PrctlFileParser.h"
 
+#define LINELENGTH 100
+
 namespace storm {
 namespace parser {
 
-PrctlFileParser::PrctlFileParser(std::string filename) {
+PrctlFileParser::PrctlFileParser(std::string filename, storm::modelChecker::AbstractModelChecker<double>* modelChecker) {
 	// Open file and initialize result.
 	std::ifstream inputFileStream(filename, std::ios::in);
 
@@ -18,8 +20,12 @@ PrctlFileParser::PrctlFileParser(std::string filename) {
 	// While this is usually not necessary, because there exist adapters that make an input stream
 	// iterable in both directions without storing it into a string, using the corresponding
 	// Boost classes gives an awful output under valgrind and is thus disabled for the time being.
-	std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
-	parse(fileContent);
+	while(!inputFileStream.eof()) {
+		char line[LINELENGTH];
+		inputFileStream.getline(line, LINELENGTH);
+
+	}
+
 }
 
 PrctlFileParser::~PrctlFileParser() {

src/parser/PrctlFileParser.h

@@ -9,6 +9,7 @@
 #define STORM_PARSER_PRCTLFILEPARSER_H_
 
 #include "PrctlParser.h"
+#include "modelchecker/AbstractModelChecker.h"
 
 namespace storm {
 namespace parser {
@@ -20,7 +21,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 PrctlFileParser: public storm::parser::PrctlParser {
+class PrctlFileParser {
 public:
 	/*!
 	 * Reads the formula from the given file and parses it into a formula tree, consisting of
@@ -31,7 +32,7 @@ public:
 	 * @param filename The name of the file to parse
 	 * @throw wrongFormatException If the input could not be parsed successfully
 	 */
-	PrctlFileParser(std::string filename);
+	PrctlFileParser(std::string filename, storm::modelChecker::AbstractModelChecker<double>* modelChecker);
 
 	/*!
 	 * Destructor.

src/parser/PrctlParser.cpp

@@ -17,6 +17,7 @@
 // Needed for file IO.
 #include <fstream>
 #include <iomanip>
+#include <map>
 
 
 // Some typedefs and namespace definitions to reduce code size.
@@ -32,19 +33,19 @@ namespace storm {
 namespace parser {
 
 template<typename Iterator, typename Skipper>
-struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::AbstractFormula<double>*(), Skipper> {
+struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::AbstractFormula<double>*(), Skipper > {
 	PrctlGrammar() : PrctlGrammar::base_type(start) {
 		freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))];
 
 		//This block defines rules for parsing state formulas
 		stateFormula %= orFormula;
 		stateFormula.name("state formula");
-		andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val =
-				phoenix::new_<storm::formula::And<double>>(qi::_val, qi::_1)];
-		andFormula.name("state formula");
 		orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
 				phoenix::new_<storm::formula::Or<double>>(qi::_val, qi::_1)];
 		orFormula.name("state formula");
+		andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val =
+				phoenix::new_<storm::formula::And<double>>(qi::_val, qi::_1)];
+		andFormula.name("state formula");
 		notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Not<double>>(qi::_1)];
 		notFormula.name("state formula");
@@ -101,11 +102,11 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 		globally = (qi::lit("G") > stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Globally<double> >(qi::_1)];
 		globally.name("path formula");
-		boundedUntil = (stateFormula >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
-				phoenix::new_<storm::formula::BoundedUntil<double>>(qi::_1, qi::_3, qi::_2)];
+		boundedUntil = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)
+				[qi::_val = phoenix::new_<storm::formula::BoundedUntil<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_3, qi::_2)];
 		boundedUntil.name("path formula");
-		until = (stateFormula >> qi::lit("U") > stateFormula)[qi::_val =
-				phoenix::new_<storm::formula::Until<double>>(qi::_1, qi::_2)];
+		until = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val =
+				phoenix::new_<storm::formula::Until<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
 		until.name("path formula");
 
 		start = (noBoundOperator | stateFormula);
@@ -132,8 +133,8 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 	qi::rule<Iterator, storm::formula::BoundedEventually<double>*(), Skipper> boundedEventually;
 	qi::rule<Iterator, storm::formula::Eventually<double>*(), Skipper> eventually;
 	qi::rule<Iterator, storm::formula::Globally<double>*(), Skipper> globally;
-	qi::rule<Iterator, storm::formula::BoundedUntil<double>*(), Skipper> boundedUntil;
-	qi::rule<Iterator, storm::formula::Until<double>*(), Skipper> until;
+	qi::rule<Iterator, storm::formula::BoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> boundedUntil;
+	qi::rule<Iterator, storm::formula::Until<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> until;
 
 	qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
 
@@ -142,7 +143,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 } //namespace storm
 } //namespace parser
 
-void storm::parser::PrctlParser::parse(std::string formulaString) {
+storm::parser::PrctlParser::PrctlParser(std::string formulaString) {
 	// Prepare iterators to input.
 	BaseIteratorType stringIteratorBegin = formulaString.begin();
 	BaseIteratorType stringIteratorEnd = formulaString.end();
@@ -194,9 +195,3 @@ void storm::parser::PrctlParser::parse(std::string formulaString) {
 
 	formula = result_pointer;
 }
-
-storm::parser::PrctlParser::PrctlParser(std::string formula) {
-	// delegate the string to the parse function
-	// this function has to be separate, as it may be called in subclasses which don't call this constructor
-	parse(formula);
-}

src/parser/PrctlParser.h

@@ -39,33 +39,6 @@ class PrctlParser : Parser
 		{
 			return this->formula;
 		}
-	
-	protected:
-		/*!
-		 * Empty constructor.
-		 *
-		 * Some subclasses do not get a formula string as input (E.g. PrctlFileParser), hence they should not
-		 * call the usual constructor of this class.
-		 *
-		 * However, this constructor should never be called directly (only during construction of an object of
-		 * a subclass), as it will not parse anything (and formula will point to nullptr then); hence, it is
-		 * protected.
-		 */
-		PrctlParser() {
-			formula = nullptr;
-		}
-
-		/*!
-		 * Does the actual parsing.
-		 *
-		 * Is to be called once in a constructor, and never from any other location.
-		 * The function is not included in the constructor, as sub classes may use constructors
-		 * that calculate the string representation of the formula (e.g. read it from a file), hence they
-		 * cannot hand it over to a constructor of this class.
-		 *
-		 * @param formula The string representation of the formula to parse
-		 */
-		void parse(std::string formula);
 
 	private:
 		storm::formula::AbstractFormula<double>* formula;

test/eigen/EigenAdapterTest.cpp

@@ -45,6 +45,8 @@ TEST(EigenAdapterTest, SimpleDenseSquareCopy) {
 			col = 0;
 		}
 	}
+
+	delete esm;
 }
 
 TEST(EigenAdapterTest, SimpleSparseSquareCopy) {
@@ -93,4 +95,6 @@ TEST(EigenAdapterTest, SimpleSparseSquareCopy) {
 			col = 0;
 		}
 	}
+
+	delete esm;
 }

test/parser/PrctlParserTest.cpp

@@ -130,6 +130,7 @@ TEST(PrctlParserTest, parseComplexFormulaTest) {
 
 }
 
+
 TEST(PrctlParserTest, wrongProbabilisticFormulaTest) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_THROW(
@@ -143,7 +144,7 @@ TEST(PrctlParserTest, wrongProbabilisticFormulaTest) {
 TEST(PrctlParserTest, wrongFormulaTest) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_THROW(
-			prctlParser = new storm::parser::PrctlFileParser("& a"),
+			prctlParser = new storm::parser::PrctlFileParser("(a | b) & ü"),
 			storm::exceptions::WrongFormatException
 	);
 	delete prctlParser;