From a3816184036f3dd2d5fd84aca22cfac6383d650d Mon Sep 17 00:00:00 2001
From: lukpo <lukas.posch@student.tugraz.at>
Date: Fri, 13 Aug 2021 09:20:16 +0200
Subject: [PATCH] added NestedPathFormulaTest to GameFormulaParserTest.cpp

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

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 = "<<p1, p2, p3>> P<0.9 [F X \"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().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