From 6dd9e09edefa8e8f9bf7bc9d00d4a1871bc1d605 Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Thu, 19 Nov 2020 18:12:54 +0100
Subject: [PATCH] added GameFormula class

---
 src/storm/logic/GameFormula.cpp | 34 ++++++++++++++++++++++++++++++++
 src/storm/logic/GameFormula.h   | 35 +++++++++++++++++++++++++++++++++
 2 files changed, 69 insertions(+)
 create mode 100644 src/storm/logic/GameFormula.cpp
 create mode 100644 src/storm/logic/GameFormula.h

diff --git a/src/storm/logic/GameFormula.cpp b/src/storm/logic/GameFormula.cpp
new file mode 100644
index 000000000..8e42f7e65
--- /dev/null
+++ b/src/storm/logic/GameFormula.cpp
@@ -0,0 +1,34 @@
+#include "storm/logic/GameFormula.h"
+
+#include "storm/logic/FormulaVisitor.h"
+
+namespace storm {
+    namespace logic {
+        GameFormula::GameFormula(Coalition coalition, std::shared_ptr<Formula const> subFormula) : coalition(coalition), subformula(subformula) {
+            STORM_PRINT_AND_LOG("CTOR subf usecount:" << subformula.use_count() << std::endl);
+            // Intentionally left empty.
+        }
+
+        bool GameFormula::isGameFormula() const {
+            return true;
+        }
+
+        Formula const& GameFormula::getSubformula() const {
+            return *subformula;
+        }
+
+        Coalition GameFormula::getCoalition() const {
+            return coalition;
+        }
+
+        boost::any GameFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+
+        std::ostream& GameFormula::writeToStream(std::ostream& out) const {
+            out << coalition;
+            this->getSubformula().writeToStream(out);
+            return out;
+        }
+    }
+}
diff --git a/src/storm/logic/GameFormula.h b/src/storm/logic/GameFormula.h
new file mode 100644
index 000000000..81384ddcf
--- /dev/null
+++ b/src/storm/logic/GameFormula.h
@@ -0,0 +1,35 @@
+#ifndef STORM_LOGIC_GAMEFORMULA_H_
+#define STORM_LOGIC_GAMEFORMULA_H_
+
+#include "storm/logic/Formula.h"
+#include "storm/logic/Coalition.h"
+#include <memory>
+
+namespace storm {
+    namespace logic {
+        class GameFormula : public Formula {
+        public:
+            GameFormula(Coalition coalition, std::shared_ptr<Formula const> subFormula);
+
+            ~GameFormula() {
+                // Intentionally left empty.
+            }
+
+            bool isGameFormula() const;
+
+            Formula const& getSubformula() const;
+            Coalition getCoalition() const;
+
+            boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const;
+
+            std::ostream& writeToStream(std::ostream& out) const;
+
+        private:
+            Coalition coalition;
+            std::shared_ptr<Formula const> subformula;
+
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_GAMEFORMULA_H_ */