Some fixes in formulas

Additional test case for reward formulas

src/formula/BoundOperator.h

@@ -116,10 +116,10 @@ public:
 	virtual std::string toString() const {
 		std::string result = "";
 		switch (comparisonOperator) {
-		case LESS: result += "<"; break;
-		case LESS_EQUAL: result += "<="; break;
-		case GREATER: result += ">"; break;
-		case GREATER_EQUAL: result += ">="; break;
+		case LESS: result += "< "; break;
+		case LESS_EQUAL: result += "<= "; break;
+		case GREATER: result += "> "; break;
+		case GREATER_EQUAL: result += ">= "; break;
 		}
 		result += std::to_string(bound);
 		result += " [";

src/formula/ProbabilisticBoundOperator.h

@@ -59,7 +59,7 @@ public:
 	 */
 	ProbabilisticBoundOperator(
 			typename BoundOperator<T>::ComparisonType comparisonRelation, T bound, PctlPathFormula<T>* pathFormula) :
-				BoundOperator<T>(BoundOperator<T>::LESS, bound, pathFormula) {
+				BoundOperator<T>(comparisonRelation, bound, pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -67,7 +67,7 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const {
-		std::string result = "P";
+		std::string result = "P ";
 		result += BoundOperator<T>::toString();
 		return result;
 	}

src/formula/RewardBoundOperator.h

@@ -57,7 +57,7 @@ public:
 	 */
 	RewardBoundOperator(
 			typename BoundOperator<T>::ComparisonType comparisonRelation, T bound, PctlPathFormula<T>* pathFormula) :
-				BoundOperator<T>(BoundOperator<T>::LESS, bound, pathFormula) {
+				BoundOperator<T>(comparisonRelation, bound, pathFormula) {
 		// Intentionally left empty
 	}
 

src/parser/PrctlParser.cpp

@@ -47,17 +47,21 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::PctlFor
 		probabilisticBoundOperator = (
 				(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 =
+				(qi::lit("P") >> qi::lit(">=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
 						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
-				("P<" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
+				(qi::lit("P") >> qi::lit("<")  >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
 								phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS, qi::_1, qi::_2)] |
-				("P<=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
+				(qi::lit("P") >> qi::lit("<=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
 						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
 				);
 		rewardBoundOperator = (
-				("R>=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
-						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
-				("R<=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
+				(qi::lit("R") >> qi::lit(">") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
+						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER, qi::_1, qi::_2)] |
+				(qi::lit("R") >> qi::lit(">=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
+								phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
+				(qi::lit("R") >> qi::lit("<") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
+										phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS, qi::_1, qi::_2)] |
+				(qi::lit("R") >> qi::lit("<=")>> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
 						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
 				);
 
@@ -76,7 +80,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::PctlFor
 				phoenix::new_<storm::formula::BoundedEventually<double>>(qi::_2, qi::_1)];
 		globally = ('G' >> stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Globally<double> >(qi::_1)];
-		until = (stateFormula >> 'U' >> stateFormula)[qi::_val =
+		until = (stateFormula >> qi::lit("U") >> stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Until<double>>(qi::_1, qi::_2)];
 		boundedUntil = (stateFormula >> "U<=" >> qi::int_ >> stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::BoundedUntil<double>>(qi::_1, qi::_3, qi::_2)];

test/parser/PrctlParserTest.cpp

@@ -26,10 +26,10 @@ TEST(PrctlParserTest, apOnly) {
 
 }
 
-TEST(PrctlParserTest, formulaTest1) {
+TEST(PrctlParserTest, propositionalFormula) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_NO_THROW(
-			prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula1.prctl")
+			prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/propositionalFormula.prctl")
 	);
 
 	ASSERT_NE(prctlParser->getFormula(), nullptr);
@@ -41,16 +41,33 @@ TEST(PrctlParserTest, formulaTest1) {
 
 }
 
-TEST(PrctlParserTest, formulaTest2) {
+TEST(PrctlParserTest, probabilisticFormula) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_NO_THROW(
-			prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula2.prctl")
+			prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticFormula.prctl")
 	);
 
 	ASSERT_NE(prctlParser->getFormula(), nullptr);
 
 
-	ASSERT_EQ(prctlParser->getFormula()->toString(), "P<0.500000 [F a]");
+	ASSERT_EQ(prctlParser->getFormula()->toString(), "P > 0.500000 [F a]");
+
+	delete prctlParser;
+
+}
+
+TEST(PrctlParserTest, rewardFormula) {
+	storm::parser::PrctlParser* prctlParser = nullptr;
+	ASSERT_NO_THROW(
+			prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardFormula.prctl")
+	);
+
+	ASSERT_NE(prctlParser->getFormula(), nullptr);
+
+	storm::formula::RewardBoundOperator<double>* op = static_cast<storm::formula::RewardBoundOperator<double>*>(prctlParser->getFormula());
+	ASSERT_EQ(storm::formula::BoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
+
+	ASSERT_EQ(prctlParser->getFormula()->toString(), "R >= 15.000000 [(a U !b)]");
 
 	delete prctlParser;
 

test/parser/prctl_files/rewardFormula.prctl

@@ -0,0 +1 @@
+R >= 15 [ a U !b ]