restricting multi-dimensional bounded until formulas to a single-dimensional one

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

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: