From 291264fff66cc89aedb569d254f4c1ee10939995 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 25 Jul 2017 15:35:35 +0200
Subject: [PATCH] restricting multi-dimensional bounded until formulas to a
 single-dimensional one

---
 src/storm/logic/BoundedUntilFormula.cpp | 4 ++++
 src/storm/logic/BoundedUntilFormula.h   | 2 ++
 2 files changed, 6 insertions(+)

diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index fecbf2673..5dca64e2b 100644
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@@ -184,6 +184,10 @@ namespace storm {
             STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants.");
         }
         
+        std::shared_ptr<BoundedUntilFormula const> BoundedUntilFormula::restrictToDimension(unsigned i) const {
+            return std::make_shared<BoundedUntilFormula const>(this->getLeftSubformula().asSharedPointer(), this->getRightSubformula().asSharedPointer(), lowerBound.at(i), upperBound.at(i), this->getTimeBoundReference(i));
+        }
+
         std::ostream& BoundedUntilFormula::writeToStream(std::ostream& out) const {
             this->getLeftSubformula().writeToStream(out);
             
diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h
index 2b2e33945..6b31301ac 100644
--- a/src/storm/logic/BoundedUntilFormula.h
+++ b/src/storm/logic/BoundedUntilFormula.h
@@ -50,6 +50,8 @@ namespace storm {
             template <typename ValueType>
             ValueType getNonStrictUpperBound(unsigned i = 0) const;
 
+            std::shared_ptr<BoundedUntilFormula const> restrictToDimension(unsigned i) const;
+            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         private: