From 02528f2bd96f6ff6797834c19fe5c1cff1487773 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Wed, 6 Feb 2013 11:04:43 +0100
Subject: [PATCH] Test cases for Prctl parser

---
 src/parser/PrctlParser.cpp                 |  4 +--
 test/parser/PrctlParserTest.cpp            | 36 ++++++++++++++++++++--
 test/parser/prctl_files/apOnly.prctl       |  1 +
 test/parser/prctl_files/testFormula.prctl  |  1 -
 test/parser/prctl_files/testFormula1.prctl |  1 +
 test/parser/prctl_files/testFormula2.prctl |  1 +
 6 files changed, 38 insertions(+), 6 deletions(-)
 create mode 100644 test/parser/prctl_files/apOnly.prctl
 delete mode 100644 test/parser/prctl_files/testFormula.prctl
 create mode 100644 test/parser/prctl_files/testFormula1.prctl
 create mode 100644 test/parser/prctl_files/testFormula2.prctl

diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 1c9c85180..298520092 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -34,7 +34,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::PctlFor
 		freeIdentifierName = qi::lexeme[(qi::alpha | qi::char_('_'))];
 
 		//This block defines rules for parsing state formulas
-		stateFormula %= (andFormula | atomicProposition | orFormula | notFormula | probabilisticBoundOperator | rewardBoundOperator);
+		stateFormula %= (andFormula | orFormula | notFormula | probabilisticBoundOperator | rewardBoundOperator | atomicProposition);
 
 		andFormula = (qi::lit("(") >> stateFormula >> qi::lit("&") >> stateFormula >> qi::lit(")"))[
 		      qi::_val = phoenix::new_<storm::formula::And<double>>(qi::_1, qi::_2)];
@@ -45,7 +45,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::PctlFor
 		atomicProposition = (freeIdentifierName)[qi::_val =
 				phoenix::new_<storm::formula::Ap<double>>(qi::_1)];
 		probabilisticBoundOperator = (
-				("P>" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
+				(qi::lit("P") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
 						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER, qi::_1, qi::_2)] |
 				("P>=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
 						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp
index bb18aaaad..5def77bf7 100644
--- a/test/parser/PrctlParserTest.cpp
+++ b/test/parser/PrctlParserTest.cpp
@@ -11,16 +11,46 @@
 #include "src/parser/PrctlParser.h"
 #include <iostream>
 
-TEST(PrctlParserTest, parseAndOutput) {
+TEST(PrctlParserTest, apOnly) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_NO_THROW(
-			prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula.prctl")
+			prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/apOnly.prctl")
 	);
 
 	ASSERT_NE(prctlParser->getFormula(), nullptr);
 
 
-	std::cout << prctlParser->getFormula()->toString();
+	ASSERT_EQ(prctlParser->getFormula()->toString(), "P");
+
+	delete prctlParser;
+
+}
+
+TEST(PrctlParserTest, formulaTest1) {
+	storm::parser::PrctlParser* prctlParser = nullptr;
+	ASSERT_NO_THROW(
+			prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula1.prctl")
+	);
+
+	ASSERT_NE(prctlParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(prctlParser->getFormula()->toString(), "!(a && b)");
+
+	delete prctlParser;
+
+}
+
+TEST(PrctlParserTest, formulaTest2) {
+	storm::parser::PrctlParser* prctlParser = nullptr;
+	ASSERT_NO_THROW(
+			prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula2.prctl")
+	);
+
+	ASSERT_NE(prctlParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(prctlParser->getFormula()->toString(), "P<0.500000 [F a]");
 
 	delete prctlParser;
 
diff --git a/test/parser/prctl_files/apOnly.prctl b/test/parser/prctl_files/apOnly.prctl
new file mode 100644
index 000000000..675f43ab4
--- /dev/null
+++ b/test/parser/prctl_files/apOnly.prctl
@@ -0,0 +1 @@
+P
\ No newline at end of file
diff --git a/test/parser/prctl_files/testFormula.prctl b/test/parser/prctl_files/testFormula.prctl
deleted file mode 100644
index fd395528e..000000000
--- a/test/parser/prctl_files/testFormula.prctl
+++ /dev/null
@@ -1 +0,0 @@
-((P>=0 [ F a ]) & P<0.5 [ G !(b) ])
\ No newline at end of file
diff --git a/test/parser/prctl_files/testFormula1.prctl b/test/parser/prctl_files/testFormula1.prctl
new file mode 100644
index 000000000..62ed48627
--- /dev/null
+++ b/test/parser/prctl_files/testFormula1.prctl
@@ -0,0 +1 @@
+!(a & b)
\ No newline at end of file
diff --git a/test/parser/prctl_files/testFormula2.prctl b/test/parser/prctl_files/testFormula2.prctl
new file mode 100644
index 000000000..947aa8543
--- /dev/null
+++ b/test/parser/prctl_files/testFormula2.prctl
@@ -0,0 +1 @@
+P > 0.5 [ F a ]
\ No newline at end of file