From 90568c54a2e0c26df415190c4126baa1053e5dc8 Mon Sep 17 00:00:00 2001
From: lukpo <lukas.posch@student.tugraz.at>
Date: Fri, 13 Aug 2021 09:15:11 +0200
Subject: [PATCH] added RewardOperatorTest to GameFormulaParserTest.cpp

---
 .../storm/parser/GameFormulaParserTest.cpp     | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp
index 72ae61070..ef4deaf22 100644
--- a/src/test/storm/parser/GameFormulaParserTest.cpp
+++ b/src/test/storm/parser/GameFormulaParserTest.cpp
@@ -201,4 +201,22 @@ TEST(GameFormulaParserTest, UntilOperatorTest) {
     EXPECT_EQ(9, rawFormula3.asBoundedUntilFormula().getUpperBound().evaluateAsInt());
 }
 
+TEST(GameFormulaParserTest, RewardOperatorTest) {
+    storm::parser::FormulaParser formulaParser;
+
+    std::string input = "<<p1, p2>> Rmin<0.9 [F \"a\"]";
+    std::shared_ptr<storm::logic::Formula const> formula(nullptr);
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
+    EXPECT_TRUE(formula->isGameFormula());
+    EXPECT_TRUE(formula->asGameFormula().getSubformula().isRewardOperatorFormula());
+    EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasBound());
+    EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasOptimalityType());
 
+    input = "<<p1, p2>> R=? [I=10]";
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
+    EXPECT_TRUE(formula->isGameFormula());
+    EXPECT_TRUE(formula->asGameFormula().getSubformula().isRewardOperatorFormula());
+    EXPECT_FALSE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasBound());
+    EXPECT_FALSE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasOptimalityType());
+    EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().isInstantaneousRewardFormula());
+}