Test cases for Prctl parser

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)] |

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;
 

test/parser/prctl_files/apOnly.prctl

@@ -0,0 +1 @@
+P

test/parser/prctl_files/testFormula.prctl

@@ -1 +0,0 @@
-((P>=0 [ F a ]) & P<0.5 [ G !(b) ])

test/parser/prctl_files/testFormula1.prctl

@@ -0,0 +1 @@
+!(a & b)

test/parser/prctl_files/testFormula2.prctl

@@ -0,0 +1 @@
+P > 0.5 [ F a ]