From d0adf9d1b3ca99e558ab612a22893b587282f98c Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Tue, 23 Apr 2013 11:39:17 +0200
Subject: [PATCH] Some more test cases and, resulting from those, minor changes
 in LTL parser.

---
 src/parser/LtlParser.cpp      | 24 +++++++++---------
 test/parser/LtlParserTest.cpp | 47 ++++++++++++++++++++++++++++++++++-
 2 files changed, 58 insertions(+), 13 deletions(-)

diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp
index bd75a73b2..30ad5eaec 100644
--- a/src/parser/LtlParser.cpp
+++ b/src/parser/LtlParser.cpp
@@ -47,27 +47,27 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::formula::ltl::Abstra
 
 		//This block defines rules for parsing state formulas
 		ltlFormula %= orFormula;
-		ltlFormula.name("state formula");
+		ltlFormula.name("LTL formula");
 		orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::Or<double>>(qi::_val, qi::_1)];
-		orFormula.name("state formula");
+		orFormula.name("LTL formula");
 		andFormula = untilFormula[qi::_val = qi::_1] > *(qi::lit("&") > untilFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::And<double>>(qi::_val, qi::_1)];
-		andFormula.name("state formula");
+		andFormula.name("LTL formula");
 		untilFormula = notFormula[qi::_val = qi::_1] >
 				*((qi::lit("U") >> qi::lit("<=") > qi::int_ > notFormula)[qi::_val = phoenix::new_<storm::formula::ltl::BoundedUntil<double>>(qi::_val, qi::_2, qi::_1)] |
 				  (qi::lit("U") > notFormula)[qi::_val = phoenix::new_<storm::formula::ltl::Until<double>>(qi::_val, qi::_1)]);
 		notFormula = atomicLtlFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicLtlFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::Not<double>>(qi::_1)];
-		notFormula.name("state formula");
+		notFormula.name("LTL formula");
 
 		//This block defines rules for "atomic" state formulas
 		//(Propositions, probabilistic/reward formulas, and state formulas in brackets)
 		atomicLtlFormula %= pathFormula | atomicProposition | qi::lit("(") >> ltlFormula >> qi::lit(")");
-		atomicLtlFormula.name("state formula");
+		atomicLtlFormula.name("LTL formula");
 		atomicProposition = (freeIdentifierName)[qi::_val =
 				phoenix::new_<storm::formula::ltl::Ap<double>>(qi::_1)];
-		atomicProposition.name("state formula");
+		atomicProposition.name("LTL formula");
 		/*probabilisticBoundOperator = (
 				(qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val =
 						phoenix::new_<storm::formula::ltl::ProbabilisticBoundOperator<double> >(storm::formula::GREATER, qi::_1, qi::_2)] |
@@ -89,16 +89,16 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::formula::ltl::Abstra
 
 		//This block defines rules for parsing probabilistic path formulas
 		pathFormula = (boundedEventually | eventually | globally);//(boundedEventually | eventually | globally | boundedUntil | until);
-		pathFormula.name("ltl formula");
+		pathFormula.name("LTL formula");
 		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::BoundedEventually<double>>(qi::_2, qi::_1)];
-		boundedEventually.name("ltl formula");
-		eventually = (qi::lit("F") > ltlFormula)[qi::_val =
+		boundedEventually.name("LTL formula");
+		eventually = (qi::lit("F") >> ltlFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::Eventually<double> >(qi::_1)];
-		eventually.name("ltl formula");
-		globally = (qi::lit("G") > ltlFormula)[qi::_val =
+		eventually.name("LTL formula");
+		globally = (qi::lit("G") >> ltlFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::Globally<double> >(qi::_1)];
-		globally.name("ltl formula");
+		globally.name("LTL formula");
 
 		start = ltlFormula;
 		start.name("LTL formula");
diff --git a/test/parser/LtlParserTest.cpp b/test/parser/LtlParserTest.cpp
index cd2a842d6..27d00f01b 100644
--- a/test/parser/LtlParserTest.cpp
+++ b/test/parser/LtlParserTest.cpp
@@ -40,6 +40,44 @@ TEST(LtlParserTest, parsePropositionalFormulaTest) {
 	delete ltlParser;
 }
 
+/*!
+ * The following test checks whether in the formula "F & b", F is correctly interpreted as proposition instead of the
+ * "Eventually" operator.
+ */
+TEST(LtlParserTest, parseAmbiguousFormulaTest) {
+	storm::parser::LtlParser* ltlParser = nullptr;
+	ASSERT_NO_THROW(
+			ltlParser = new storm::parser::LtlParser("F & b")
+	);
+
+	ASSERT_NE(ltlParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(ltlParser->getFormula()->toString(), "(F & b)");
+
+	delete ltlParser->getFormula();
+	delete ltlParser;
+}
+
+/*!
+ * The following test checks whether in the formula "F F", F is interpreted as "eventually" operator or atomic proposition,
+ * depending where it occurs.
+ */
+TEST(LtlParserTest, parseAmbiguousFormulaTest2) {
+	storm::parser::LtlParser* ltlParser = nullptr;
+	ASSERT_NO_THROW(
+			ltlParser = new storm::parser::LtlParser("F F")
+	);
+
+	ASSERT_NE(ltlParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(ltlParser->getFormula()->toString(), "F F");
+
+	delete ltlParser->getFormula();
+	delete ltlParser;
+}
+
 TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) {
 	storm::parser::LtlParser* ltlParser = nullptr;
 	ASSERT_NO_THROW(
@@ -102,6 +140,13 @@ TEST(LtlParserTest, parseComplexFormulaTest) {
 	ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", ltlParser->getFormula()->toString());
 	delete ltlParser->getFormula();
 	delete ltlParser;
-
 }
 
+TEST(LtlParserTest, wrongFormulaTest) {
+	storm::parser::LtlParser* ltlParser = nullptr;
+	ASSERT_THROW(
+			ltlParser = new storm::parser::LtlParser("(a | b) & +"),
+			storm::exceptions::WrongFormatException
+	);
+	delete ltlParser;
+}