From a08db1b2cf158b20c19bde373e8c4e5fec5602c3 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Thu, 16 May 2013 16:32:31 +0200
Subject: [PATCH] Changed prctl parser.

Now, only complete lines will be matched (Before, the parser returned
a result when a prefix could be matched); furthermore, comments are
supported better.
---
 src/parser/PrctlFileParser.cpp | 13 +++++--------
 src/parser/PrctlParser.cpp     | 18 +++++++++---------
 src/parser/PrctlParser.h       | 10 ++++++++++
 3 files changed, 24 insertions(+), 17 deletions(-)

diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp
index 0f7f877f1..4fa7a13d3 100644
--- a/src/parser/PrctlFileParser.cpp
+++ b/src/parser/PrctlFileParser.cpp
@@ -13,8 +13,6 @@
 #include "modelchecker/GmmxxDtmcPrctlModelChecker.h"
 #include "modelchecker/GmmxxMdpPrctlModelChecker.h"
 
-#include <boost/algorithm/string.hpp>
-
 namespace storm {
 namespace parser {
 
@@ -41,13 +39,12 @@ std::list<storm::property::prctl::AbstractPrctlFormula<double>*> PrctlFileParser
 		std::string line;
 		//The while loop reads the input file line by line
 		while (std::getline(inputFileStream, line)) {
-			boost::algorithm::trim(line);
-			if ((line.length() == 0) || ((line[0] == '/') && (line[1] == '/'))) {
-				// ignore empty lines and lines starting with //
-				continue;
-			}
 			PrctlParser parser(line);
-			result.push_back(parser.getFormula());
+			if (!parser.parsedComment()) {
+				//lines containing comments will be skipped.
+				LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + parser.getFormula()->toString() + "\"");
+				result.push_back(parser.getFormula());
+			}
 		}
 	}
 
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 18f470660..446a6feb5 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -43,6 +43,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 				(qi::lit(">"))[qi::_val = storm::property::GREATER] |
 				(qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] |
 				(qi::lit("<"))[qi::_val = storm::property::LESS]);
+		//Comment: Empty line or line starting with "//"
 		comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr];
 
 		//This block defines rules for parsing state formulas
@@ -70,7 +71,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 						phoenix::new_<storm::property::prctl::ProbabilisticBoundOperator<double> >(qi::_1, qi::_2, qi::_3, true)] |
 				(qi::lit("P") >> qi::lit("max") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
 						phoenix::new_<storm::property::prctl::ProbabilisticBoundOperator<double> >(qi::_1, qi::_2, qi::_3, false)] |
-				(qi::lit("P") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
+				(qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
 						phoenix::new_<storm::property::prctl::ProbabilisticBoundOperator<double> >(qi::_1, qi::_2, qi::_3)]
 				);
 
@@ -142,11 +143,17 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		instantaneousReward.name("path formula (for reward operator)");
 		steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_<storm::property::prctl::SteadyStateReward<double>>()];
 
-		start = (comment | noBoundOperator | stateFormula) >> qi::eoi;
+		formula = (noBoundOperator | stateFormula);
+		formula.name("PRCTL formula");
+
+		start = (((formula) > (comment | qi::eps))[qi::_val = qi::_1] |
+				 comment
+				 ) > qi::eoi;
 		start.name("PRCTL formula");
 	}
 
 	qi::rule<Iterator, storm::property::prctl::AbstractPrctlFormula<double>*(), Skipper> start;
+	qi::rule<Iterator, storm::property::prctl::AbstractPrctlFormula<double>*(), Skipper> formula;
 	qi::rule<Iterator, storm::property::prctl::AbstractPrctlFormula<double>*(), Skipper> comment;
 
 	qi::rule<Iterator, storm::property::prctl::AbstractStateFormula<double>*(), Skipper> stateFormula;
@@ -228,12 +235,5 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) {
 		throw storm::exceptions::WrongFormatException() << msg.str();
 	}
 
-	// The syntax can be so wrong that no rule can be matched at all
-	// In that case, no expectation failure is thrown, but the parser just returns nullptr
-	// Then, of course the result is not usable, hence we throw a WrongFormatException, too.
-	if (positionIteratorBegin != positionIteratorEnd) {
-		throw storm::exceptions::WrongFormatException() << "Syntax error in formula";
-	}
-
 	formula = result_pointer;
 }
diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h
index 3778b862a..7e2b3d13d 100644
--- a/src/parser/PrctlParser.h
+++ b/src/parser/PrctlParser.h
@@ -38,6 +38,16 @@ class PrctlParser : Parser {
 			return this->formula;
 		}
 
+		/*!
+		 * Checks whether the line which was parsed was a comment line; also returns true if the line was empty (as the semantics are
+		 * the same)
+		 *
+		 * @return True if the parsed line consisted completely of a (valid) comment, false otherwise.
+		 */
+		bool parsedComment() {
+			return (formula == nullptr);
+		}
+
 	private:
 		storm::property::prctl::AbstractPrctlFormula<double>* formula;