created class BoundedGloballyFormula

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;
+        }
+    }
+}

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

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;
         }

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;

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;

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;