From c14292218229fe91a2474e84ff890833eb2a6fa3 Mon Sep 17 00:00:00 2001
From: Lukas Posch <lukas.posch@student.tugraz.at>
Date: Thu, 4 Mar 2021 16:12:48 +0100
Subject: [PATCH] Set up BoundedGloballyFormula to methods of Formula.*

---
 src/storm/logic/Formula.cpp | 17 +++++++++++++----
 src/storm/logic/Formula.h   |  5 ++++-
 2 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index d5359875a..70379b8ba 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -79,10 +79,6 @@ namespace storm {
             return false;
         }
 
-        bool Formula::isBoundedGloballyFormula() const {
-            return false;
-        }
-
         bool Formula::isGloballyFormula() const {
             return false;
         }
@@ -119,6 +115,10 @@ namespace storm {
             return false;
         }
 
+        bool Formula::isBoundedGloballyFormula() const {
+            return false;
+        }
+
         bool Formula::isLongRunAverageOperatorFormula() const {
             return false;
         }
@@ -377,6 +377,15 @@ namespace storm {
             return dynamic_cast<NextFormula const&>(*this);
         }
 
+        // TODO: find out why these casts are not valid
+        BoundedGloballyFormula& Formula::asBoundedGloballyFormula() {
+            return dynamic_cast<BoundedGloballyFormula&>(*this);
+        }
+
+        BoundedGloballyFormula const& Formula::asBoundedGloballyFormula() const {
+            return dynamic_cast<BoundedGloballyFormula const &>(*this);
+        }
+
         LongRunAverageOperatorFormula& Formula::asLongRunAverageOperatorFormula() {
             return dynamic_cast<LongRunAverageOperatorFormula&>(*this);
         }
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 24c288619..62aab0dde 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -173,7 +173,10 @@ namespace storm {
             
             NextFormula& asNextFormula();
             NextFormula const& asNextFormula() const;
-            
+
+            BoundedGloballyFormula& asBoundedGloballyFormula();
+            BoundedGloballyFormula const& asBoundedGloballyFormula() const;
+
             LongRunAverageOperatorFormula& asLongRunAverageOperatorFormula();
             LongRunAverageOperatorFormula const& asLongRunAverageOperatorFormula() const;