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::restrictToDimension(unsigned i) const { + return std::make_shared(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 ValueType getNonStrictUpperBound(unsigned i = 0) const; + std::shared_ptr restrictToDimension(unsigned i) const; + virtual std::ostream& writeToStream(std::ostream& out) const override; private: