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 = "<> Rmin<0.9 [F \"a\"]"; + std::shared_ptr 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 = "<> 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()); +}