diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index 33633b319..ccafab82c 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -136,6 +136,10 @@ namespace storm { } } + std::vector const& CumulativeRewardFormula::getBounds() const { + return bounds; + } + void CumulativeRewardFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) { STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants."); } @@ -149,8 +153,12 @@ namespace storm { } + std::shared_ptr CumulativeRewardFormula::stripRewardAccumulation() const { + return std::make_shared(bounds, timeBoundReferences); + } + std::shared_ptr CumulativeRewardFormula::restrictToDimension(unsigned i) const { - return std::make_shared(bounds.at(i), getTimeBoundReference(i)); + return std::make_shared(bounds.at(i), getTimeBoundReference(i), rewardAccumulation); } std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const { diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h index cccd1ac9e..80924865a 100644 --- a/src/storm/logic/CumulativeRewardFormula.h +++ b/src/storm/logic/CumulativeRewardFormula.h @@ -48,8 +48,11 @@ namespace storm { template ValueType getNonStrictBound() const; + std::vector const& getBounds() const; + bool hasRewardAccumulation() const; RewardAccumulation const& getRewardAccumulation() const; + std::shared_ptr stripRewardAccumulation() const; std::shared_ptr restrictToDimension(unsigned i) const; diff --git a/src/storm/logic/LongRunAverageRewardFormula.cpp b/src/storm/logic/LongRunAverageRewardFormula.cpp index c36dab8a9..294c8de95 100644 --- a/src/storm/logic/LongRunAverageRewardFormula.cpp +++ b/src/storm/logic/LongRunAverageRewardFormula.cpp @@ -24,6 +24,10 @@ namespace storm { return rewardAccumulation.get(); } + std::shared_ptr LongRunAverageRewardFormula::stripRewardAccumulation() const { + return std::make_shared(); + } + boost::any LongRunAverageRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } diff --git a/src/storm/logic/LongRunAverageRewardFormula.h b/src/storm/logic/LongRunAverageRewardFormula.h index 03f1c3684..45bbe3de5 100644 --- a/src/storm/logic/LongRunAverageRewardFormula.h +++ b/src/storm/logic/LongRunAverageRewardFormula.h @@ -19,7 +19,8 @@ namespace storm { virtual bool isRewardPathFormula() const override; bool hasRewardAccumulation() const; RewardAccumulation const& getRewardAccumulation() const; - + std::shared_ptr stripRewardAccumulation() const; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/storm/logic/TotalRewardFormula.cpp b/src/storm/logic/TotalRewardFormula.cpp index 4d1df7e0d..fb6f60873 100644 --- a/src/storm/logic/TotalRewardFormula.cpp +++ b/src/storm/logic/TotalRewardFormula.cpp @@ -24,6 +24,10 @@ namespace storm { return rewardAccumulation.get(); } + std::shared_ptr TotalRewardFormula::stripRewardAccumulation() const { + return std::make_shared(); + } + boost::any TotalRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } diff --git a/src/storm/logic/TotalRewardFormula.h b/src/storm/logic/TotalRewardFormula.h index a11fb3b03..1fa366723 100644 --- a/src/storm/logic/TotalRewardFormula.h +++ b/src/storm/logic/TotalRewardFormula.h @@ -20,6 +20,7 @@ namespace storm { virtual bool isRewardPathFormula() const override; bool hasRewardAccumulation() const; RewardAccumulation const& getRewardAccumulation() const; + std::shared_ptr stripRewardAccumulation() const; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;