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

---
 src/storm/logic/FragmentChecker.cpp | 10 ++++++++++
 src/storm/logic/FragmentChecker.h   |  1 +
 2 files changed, 11 insertions(+)

diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp
index 06772b6ba..df79d22a5 100644
--- a/src/storm/logic/FragmentChecker.cpp
+++ b/src/storm/logic/FragmentChecker.cpp
@@ -57,6 +57,16 @@ namespace storm {
             return inherited.getSpecification().areBooleanLiteralFormulasAllowed();
         }
 
+        boost::any FragmentChecker::visit(BoundedGloballyFormula const& f, boost::any const& data) const {
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areGloballyFormulasAllowed();
+            if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
+                result = result && !f.getSubformula().isPathFormula();
+            }
+            result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            return result;
+        }
+
         boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed();
diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h
index c6e6100ee..0b0d179aa 100644
--- a/src/storm/logic/FragmentChecker.h
+++ b/src/storm/logic/FragmentChecker.h
@@ -16,6 +16,7 @@ namespace storm {
             virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;