From c1ab2ca8d9ade908ab1483161df120738f941274 Mon Sep 17 00:00:00 2001
From: Lukas Posch <lukas.posch@student.tugraz.at>
Date: Thu, 4 Mar 2021 14:31:30 +0100
Subject: [PATCH] created class BoundedGloballyFormula

---
 src/storm/logic/BoundedGloballyFormula.cpp    | 28 +++++++++++++++++++
 src/storm/logic/BoundedGloballyFormula.h      | 25 +++++++++++++++++
 src/storm/logic/Formula.cpp                   |  4 +++
 src/storm/logic/Formula.h                     |  1 +
 src/storm/logic/FormulaVisitor.h              |  1 +
 src/storm/logic/FormulasForwardDeclarations.h |  1 +
 6 files changed, 60 insertions(+)
 create mode 100644 src/storm/logic/BoundedGloballyFormula.cpp
 create mode 100644 src/storm/logic/BoundedGloballyFormula.h

diff --git a/src/storm/logic/BoundedGloballyFormula.cpp b/src/storm/logic/BoundedGloballyFormula.cpp
new file mode 100644
index 000000000..e397117ef
--- /dev/null
+++ b/src/storm/logic/BoundedGloballyFormula.cpp
@@ -0,0 +1,28 @@
+#include "storm/logic/BoundedGloballyFormula.h"
+#include "storm/logic/FormulaVisitor.h"
+
+namespace storm {
+    namespace logic {
+        BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr<Formula const> const& subformula) : UnaryPathFormula(subformula) {
+            // Intentionally left empty.
+        }
+
+        bool BoundedGloballyFormula::isBoundedGloballyFormula() const {
+            return true;
+        }
+
+        bool BoundedGloballyFormula::isProbabilityPathFormula() const {
+            return true;
+        }
+
+        boost::any BoundedGloballyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+
+        std::ostream& BoundedGloballyFormula::writeToStream(std::ostream& out) const {
+            out << "G < ";
+            this->getSubformula().writeToStream(out);
+            return out;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storm/logic/BoundedGloballyFormula.h b/src/storm/logic/BoundedGloballyFormula.h
new file mode 100644
index 000000000..97f7e26fb
--- /dev/null
+++ b/src/storm/logic/BoundedGloballyFormula.h
@@ -0,0 +1,25 @@
+#ifndef STORM_BOUNDEDGLOBALLYFORMULA_H
+#define STORM_BOUNDEDGLOBALLYFORMULA_H
+
+#include "storm/logic/UnaryPathFormula.h"
+
+namespace storm {
+    namespace logic {
+        class BoundedGloballyFormula : public UnaryPathFormula {
+        public:
+            BoundedGloballyFormula(std::shared_ptr<Formula const> const &subformula);
+
+            virtual ~BoundedGloballyFormula() {
+                // Intentionally left empty.
+            }
+
+            virtual bool isBoundedGloballyFormula() const override;
+            virtual bool isProbabilityPathFormula() const override;
+
+            virtual boost::any accept(FormulaVisitor const &visitor, boost::any const &data) const override;
+            virtual std::ostream &writeToStream(std::ostream &out) const override;
+        };
+    }
+}
+
+#endif //STORM_BOUNDEDGLOBALLYFORMULA_H
diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index d8b399e34..d5359875a 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -79,6 +79,10 @@ namespace storm {
             return false;
         }
 
+        bool Formula::isBoundedGloballyFormula() const {
+            return false;
+        }
+
         bool Formula::isGloballyFormula() const {
             return false;
         }
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 294637c2e..24c288619 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -71,6 +71,7 @@ namespace storm {
             virtual bool isGloballyFormula() const;
             virtual bool isEventuallyFormula() const;
             virtual bool isReachabilityProbabilityFormula() const;
+            virtual bool isBoundedGloballyFormula() const;
 
             // Reward formulas.
             virtual bool isCumulativeRewardFormula() const;
diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h
index 6bf5b8c50..23673ff50 100644
--- a/src/storm/logic/FormulaVisitor.h
+++ b/src/storm/logic/FormulaVisitor.h
@@ -16,6 +16,7 @@ namespace storm {
             virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const = 0;
diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h
index 2d1661418..1a6611f13 100644
--- a/src/storm/logic/FormulasForwardDeclarations.h
+++ b/src/storm/logic/FormulasForwardDeclarations.h
@@ -11,6 +11,7 @@ namespace storm {
         class BinaryPathFormula;
         class BinaryStateFormula;
         class BooleanLiteralFormula;
+        class BoundedGloballyFormula;
         class BoundedUntilFormula;
         class ConditionalFormula;
         class CumulativeRewardFormula;