diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index ef4deaf22..a5fa7036a 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -220,3 +220,15 @@ TEST(GameFormulaParserTest, RewardOperatorTest) { EXPECT_FALSE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasOptimalityType()); EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().isInstantaneousRewardFormula()); } + +TEST(GameFormulaParserTest, ConditionalProbabilityTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "<> P<0.9 [F \"a\" || F \"b\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asGameFormula().getSubformula().asProbabilityOperatorFormula(); + EXPECT_TRUE(probFormula.getSubformula().isConditionalProbabilityFormula()); +}