diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index c2d3291a5..d6b6bff3b 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -105,9 +105,7 @@ TEST(GameFormulaParserTest, PlayersCoalitionTest) { std::ostringstream stream; stream << playerCoalition; std::string playerCoalitionString = stream.str(); - std::string playerWithoutWhiteSpace = "p1,p2,p3,p4,p5"; - EXPECT_EQ(playerWithoutWhiteSpace, playerCoalitionString); } @@ -134,30 +132,39 @@ TEST(GameFormulaParserTest, UntilOperatorTest) { std::string input = "<

> Pmax=? [\"a\" U \"b\"]"; std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); auto const& gameFormula1 = formula->asGameFormula(); auto const& probFormula1 = gameFormula1.getSubformula(); + EXPECT_TRUE(probFormula1.isProbabilityOperatorFormula()); auto const& rawFormula1 = probFormula1.asProbabilityOperatorFormula().getSubformula(); EXPECT_TRUE(rawFormula1.isUntilFormula()); EXPECT_FALSE(rawFormula1.isBoundedUntilFormula()); - input = "<

> Pmax=? [\"a\" U <= 4 \"b\"]"; + input = "<

> Pmax=? [ \"a\" U <= 4 \"b\" ]"; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); auto const& gameFormula2 = formula->asGameFormula(); auto const& probFormula2 = gameFormula2.getSubformula(); + EXPECT_TRUE(probFormula2.isProbabilityOperatorFormula()); auto const& rawFormula2 = probFormula2.asProbabilityOperatorFormula().getSubformula(); EXPECT_TRUE(rawFormula2.isBoundedUntilFormula()); EXPECT_TRUE(rawFormula2.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); - EXPECT_EQ(0, rawFormula2.asBoundedUntilFormula().getLowerBound().evaluateAsInt()); + EXPECT_FALSE(rawFormula2.asBoundedUntilFormula().hasLowerBound()); + EXPECT_TRUE(rawFormula2.asBoundedUntilFormula().hasUpperBound()); EXPECT_EQ(4, rawFormula2.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); - input = "<> Pmin=? [ (a&b) U [5,9] (b|c) ]"; + input = "<> Pmin=? [ \"a\" & \"b\" U [5,9] \"c\" ] "; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); auto const& gameFormula3 = formula->asGameFormula(); auto const& probFormula3 = gameFormula3.getSubformula(); + EXPECT_TRUE(probFormula3.isProbabilityOperatorFormula()); auto const& rawFormula3 = probFormula3.asProbabilityOperatorFormula().getSubformula(); EXPECT_TRUE(rawFormula3.isBoundedUntilFormula()); EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().hasLowerBound()); EXPECT_EQ(5, rawFormula3.asBoundedUntilFormula().getLowerBound().evaluateAsInt()); + EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().hasUpperBound()); EXPECT_EQ(9, rawFormula3.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); }