From 1b81c009c107f965ae798538ba29f36196c44c9a Mon Sep 17 00:00:00 2001
From: lukpo <lukas.posch@student.tugraz.at>
Date: Thu, 12 Aug 2021 08:22:38 +0200
Subject: [PATCH] WIP added GameFormulaParserTest.cpp

---
 .../storm/parser/GameFormulaParserTest.cpp    | 62 +++++++++++++++++++
 1 file changed, 62 insertions(+)
 create mode 100644 src/test/storm/parser/GameFormulaParserTest.cpp

diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp
new file mode 100644
index 000000000..2f867a494
--- /dev/null
+++ b/src/test/storm/parser/GameFormulaParserTest.cpp
@@ -0,0 +1,62 @@
+#include "test/storm_gtest.h"
+#include "storm-config.h"
+#include "storm-parsers/parser/FormulaParser.h"
+#include "storm/logic/FragmentSpecification.h"
+#include "storm/exceptions/WrongFormatException.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+
+// TODO: write this to <<player>> inputs (games)!
+
+TEST(GameFormulaParserTest, LabelTest) {
+    storm::parser::FormulaParser formulaParser;
+
+    std::string input = "<<player>> \"label\"";
+    std::shared_ptr<storm::logic::Formula const> formula(nullptr);
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
+
+    EXPECT_TRUE(formula->isAtomicLabelFormula());
+}
+
+TEST(GameFormulaParserTest, ComplexLabelTest) {
+    storm::parser::FormulaParser formulaParser;
+
+    std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\"";
+    std::shared_ptr<storm::logic::Formula const> formula(nullptr);
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
+
+    EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
+    EXPECT_TRUE(formula->isBinaryBooleanStateFormula());
+}
+
+TEST(GameFormulaParserTest, ExpressionTest) {
+    std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
+    manager->declareBooleanVariable("x");
+    manager->declareIntegerVariable("y");
+
+    storm::parser::FormulaParser formulaParser(manager);
+
+    std::string input = "!(x | y > 3)";
+    std::shared_ptr<storm::logic::Formula const> formula(nullptr);
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
+
+    EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
+    EXPECT_TRUE(formula->isUnaryBooleanStateFormula());
+}
+
+TEST(GameFormulaParserTest, LabelAndExpressionTest) {
+    std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
+    manager->declareBooleanVariable("x");
+    manager->declareIntegerVariable("y");
+
+    storm::parser::FormulaParser formulaParser(manager);
+
+    std::string input = "!\"a\" | x | y > 3";
+    std::shared_ptr<storm::logic::Formula const> formula(nullptr);
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
+
+    EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
+
+    input = "x | y > 3 | !\"a\"";
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
+    EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
+}
\ No newline at end of file