diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index a5fa7036a..ede75a6ad 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -232,3 +232,15 @@ TEST(GameFormulaParserTest, ConditionalProbabilityTest) { storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asGameFormula().getSubformula().asProbabilityOperatorFormula(); EXPECT_TRUE(probFormula.getSubformula().isConditionalProbabilityFormula()); } + +TEST(GameFormulaParserTest, NestedPathFormulaTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "<> P<0.9 [F X \"a\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); + ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isNextFormula()); +} \ No newline at end of file