diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 97c768944..6054e7cd3 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -285,7 +285,11 @@ namespace storm { out << ", "; } if (this->getTimeBoundReference(i).isRewardBound()) { - out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + out << "rew"; + if (this->getTimeBoundReference(i).hasRewardAccumulation()) { + out << "[" << this->getTimeBoundReference(i).getRewardAccumulation() << "]"; + } + out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; } else if (this->getTimeBoundReference(i).isStepBound()) { out << "steps"; //} else if (this->getTimeBoundReference(i).isStepBound()) diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index d97dd41d6..3e24d92c0 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -70,7 +70,11 @@ namespace storm { boost::any CloneVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); - return std::static_pointer_cast(std::make_shared(subformula, f.getContext())); + if (f.hasRewardAccumulation()) { + return std::static_pointer_cast(std::make_shared(subformula, f.getContext(), f.getRewardAccumulation())); + } else { + return std::static_pointer_cast(std::make_shared(subformula, f.getContext())); + } } boost::any CloneVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index 19a60a623..bbf21cbf0 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -9,11 +9,11 @@ namespace storm { namespace logic { - CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference) : timeBoundReferences({timeBoundReference}), bounds({bound}) { + CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference, boost::optional rewardAccumulation) : timeBoundReferences({timeBoundReference}), bounds({bound}), rewardAccumulation(rewardAccumulation) { // Intentionally left empty. } - CumulativeRewardFormula::CumulativeRewardFormula(std::vector const& bounds, std::vector const& timeBoundReferences) : timeBoundReferences(timeBoundReferences), bounds(bounds) { + CumulativeRewardFormula::CumulativeRewardFormula(std::vector const& bounds, std::vector const& timeBoundReferences, boost::optional rewardAccumulation) : timeBoundReferences(timeBoundReferences), bounds(bounds), rewardAccumulation(rewardAccumulation) { STORM_LOG_ASSERT(this->timeBoundReferences.size() == this->bounds.size(), "Number of time bounds and number of time bound references does not match."); STORM_LOG_ASSERT(!this->timeBoundReferences.empty(), "No time bounds given."); @@ -137,12 +137,24 @@ namespace storm { STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants."); } + bool CumulativeRewardFormula::hasRewardAccumulation() const { + return rewardAccumulation.is_initialized(); + } + + RewardAccumulation const& CumulativeRewardFormula::getRewardAccumulation() const { + return rewardAccumulation.get(); + } + + std::shared_ptr CumulativeRewardFormula::restrictToDimension(unsigned i) const { return std::make_shared(bounds.at(i), getTimeBoundReference(i)); } std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const { out << "C"; + if (hasRewardAccumulation()) { + out << "[" << getRewardAccumulation() << "]"; + } if (this->isMultiDimensional()) { out << "^{"; } @@ -151,7 +163,11 @@ namespace storm { out << ", "; } if (this->getTimeBoundReference(i).isRewardBound()) { - out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + out << "rew"; + if (this->getTimeBoundReference(i).hasRewardAccumulation()) { + out << "[" << this->getTimeBoundReference(i).getRewardAccumulation() << "]"; + } + out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; } else if (this->getTimeBoundReference(i).isStepBound()) { out << "steps"; //} else if (this->getTimeBoundReference(i).isStepBound()) diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h index e40370b07..4c436037e 100644 --- a/src/storm/logic/CumulativeRewardFormula.h +++ b/src/storm/logic/CumulativeRewardFormula.h @@ -10,8 +10,8 @@ namespace storm { namespace logic { class CumulativeRewardFormula : public PathFormula { public: - CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time)); - CumulativeRewardFormula(std::vector const& bounds, std::vector const& timeBoundReferences); + CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time), boost::optional rewardAccumulation = boost::none); + CumulativeRewardFormula(std::vector const& bounds, std::vector const& timeBoundReferences, boost::optional rewardAccumulation = boost::none); virtual ~CumulativeRewardFormula() = default; @@ -47,6 +47,9 @@ namespace storm { template ValueType getNonStrictBound() const; + bool hasRewardAccumulation() const; + RewardAccumulation const& getRewardAccumulation() const; + std::shared_ptr restrictToDimension(unsigned i) const; private: @@ -54,6 +57,8 @@ namespace storm { std::vector timeBoundReferences; std::vector bounds; + boost::optional rewardAccumulation; + }; } } diff --git a/src/storm/logic/EventuallyFormula.cpp b/src/storm/logic/EventuallyFormula.cpp index 2f1243f8a..863b977fd 100644 --- a/src/storm/logic/EventuallyFormula.cpp +++ b/src/storm/logic/EventuallyFormula.cpp @@ -6,7 +6,7 @@ namespace storm { namespace logic { - EventuallyFormula::EventuallyFormula(std::shared_ptr const& subformula, FormulaContext context) : UnaryPathFormula(subformula), context(context) { + EventuallyFormula::EventuallyFormula(std::shared_ptr const& subformula, FormulaContext context, boost::optional rewardAccumulation) : UnaryPathFormula(subformula), context(context), rewardAccumulation(rewardAccumulation) { STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward || context == FormulaContext::Time, storm::exceptions::InvalidPropertyException, "Invalid context for formula."); } @@ -42,6 +42,14 @@ namespace storm { return this->isReachabilityTimeFormula(); } + bool EventuallyFormula::hasRewardAccumulation() const { + return rewardAccumulation.is_initialized(); + } + + RewardAccumulation const& EventuallyFormula::getRewardAccumulation() const { + return rewardAccumulation.get(); + } + boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } @@ -49,6 +57,9 @@ namespace storm { std::ostream& EventuallyFormula::writeToStream(std::ostream& out) const { out << "F "; this->getSubformula().writeToStream(out); + if (hasRewardAccumulation()) { + out << "[" << getRewardAccumulation() << "]"; + } return out; } } diff --git a/src/storm/logic/EventuallyFormula.h b/src/storm/logic/EventuallyFormula.h index 9cc4d853d..5fa30da6d 100644 --- a/src/storm/logic/EventuallyFormula.h +++ b/src/storm/logic/EventuallyFormula.h @@ -1,14 +1,17 @@ #ifndef STORM_LOGIC_EVENTUALLYFORMULA_H_ #define STORM_LOGIC_EVENTUALLYFORMULA_H_ +#include + #include "storm/logic/UnaryPathFormula.h" #include "storm/logic/FormulaContext.h" +#include "storm/logic/RewardAccumulation.h" namespace storm { namespace logic { class EventuallyFormula : public UnaryPathFormula { public: - EventuallyFormula(std::shared_ptr const& subformula, FormulaContext context = FormulaContext::Probability); + EventuallyFormula(std::shared_ptr const& subformula, FormulaContext context = FormulaContext::Probability, boost::optional rewardAccumulation = boost::none); virtual ~EventuallyFormula() { // Intentionally left empty. @@ -27,9 +30,12 @@ namespace storm { virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; + bool hasRewardAccumulation() const; + RewardAccumulation const& getRewardAccumulation() const; private: FormulaContext context; + boost::optional rewardAccumulation; }; } } diff --git a/src/storm/logic/RewardAccumulation.cpp b/src/storm/logic/RewardAccumulation.cpp new file mode 100644 index 000000000..e7996f0e0 --- /dev/null +++ b/src/storm/logic/RewardAccumulation.cpp @@ -0,0 +1,47 @@ +#include "storm/logic/RewardAccumulation.h" + +namespace storm { + namespace logic { + + RewardAccumulation::RewardAccumulation(bool steps, bool time, bool exit) : steps(steps), time(time), exit(exit){ + // Intentionally left empty + } + + bool RewardAccumulation::isStepsSet() const { + return steps; + } + + bool RewardAccumulation::isTimeSet() const { + return time; + } + + bool RewardAccumulation::isExitSet() const { + return exit; + } + + std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc) { + bool hasEntry = false; + if (acc.isStepsSet()) { + out << "steps"; + hasEntry = true; + } + if (acc.isTimeSet()) { + if (hasEntry) { + out << ", "; + } + out << "time"; + hasEntry = true; + } + if (acc.isExitSet()) { + if (hasEntry) { + out << ", "; + } + out << "exit"; + hasEntry = true; + } + + return out; + } + + } +} diff --git a/src/storm/logic/RewardAccumulation.h b/src/storm/logic/RewardAccumulation.h new file mode 100644 index 000000000..89c18b017 --- /dev/null +++ b/src/storm/logic/RewardAccumulation.h @@ -0,0 +1,24 @@ +#pragma once +#include + +namespace storm { + namespace logic { + + class RewardAccumulation { + public: + RewardAccumulation(bool steps, bool time, bool exit); + RewardAccumulation(RewardAccumulation const& other) = default; + + bool isStepsSet() const; // If set, choice rewards and transition rewards are accumulated upon taking the transition + bool isTimeSet() const; // If set, state rewards are accumulated over time (assuming 0 time passes in discrete-time model states) + bool isExitSet() const; // If set, state rewards are accumulated upon exiting the state + + private: + bool time, steps, exit; + }; + + std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc); + + } +} + diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h index 0bd6aba0c..23f850105 100644 --- a/src/storm/logic/TimeBoundType.h +++ b/src/storm/logic/TimeBoundType.h @@ -1,5 +1,9 @@ #pragma once +#include + +#include "storm/logic/RewardAccumulation.h" + namespace storm { namespace logic { @@ -13,14 +17,15 @@ namespace storm { class TimeBoundReference { TimeBoundType type; std::string rewardName; - + boost::optional rewardAccumulation; + public: explicit TimeBoundReference(TimeBoundType t) : type(t) { // For rewards, use the other constructor. assert(t != TimeBoundType::Reward); } - explicit TimeBoundReference(std::string const& rewardName) : type(TimeBoundType::Reward), rewardName(rewardName) { + explicit TimeBoundReference(std::string const& rewardName, boost::optional rewardAccumulation = boost::none) : type(TimeBoundType::Reward), rewardName(rewardName), rewardAccumulation(rewardAccumulation) { assert(rewardName != ""); // Empty reward name is reserved. } @@ -44,6 +49,17 @@ namespace storm { assert(isRewardBound()); return rewardName; } + + bool hasRewardAccumulation() const { + assert(isRewardBound()); + return rewardAccumulation.is_initialized(); + } + + RewardAccumulation const& getRewardAccumulation() const { + assert(isRewardBound()); + return rewardAccumulation.get(); + } + }; diff --git a/src/storm/logic/TotalRewardFormula.cpp b/src/storm/logic/TotalRewardFormula.cpp index 18c79cd67..6136581a3 100644 --- a/src/storm/logic/TotalRewardFormula.cpp +++ b/src/storm/logic/TotalRewardFormula.cpp @@ -4,7 +4,7 @@ namespace storm { namespace logic { - TotalRewardFormula::TotalRewardFormula() { + TotalRewardFormula::TotalRewardFormula(boost::optional rewardAccumulation) : rewardAccumulation(rewardAccumulation) { // Intentionally left empty. } @@ -16,6 +16,14 @@ namespace storm { return true; } + bool TotalRewardFormula::hasRewardAccumulation() const { + return rewardAccumulation.is_initialized(); + } + + RewardAccumulation const& TotalRewardFormula::getRewardAccumulation() const { + return rewardAccumulation.get(); + } + 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 90caee9e7..a11fb3b03 100644 --- a/src/storm/logic/TotalRewardFormula.h +++ b/src/storm/logic/TotalRewardFormula.h @@ -1,15 +1,16 @@ #ifndef STORM_LOGIC_TOTALREWARDFORMULA_H_ #define STORM_LOGIC_TOTALREWARDFORMULA_H_ -#include +#include +#include "storm/logic/RewardAccumulation.h" #include "storm/logic/PathFormula.h" namespace storm { namespace logic { class TotalRewardFormula : public PathFormula { public: - TotalRewardFormula(); + TotalRewardFormula(boost::optional rewardAccumulation = boost::none); virtual ~TotalRewardFormula() { // Intentionally left empty. @@ -17,11 +18,15 @@ namespace storm { virtual bool isTotalRewardFormula() const override; virtual bool isRewardPathFormula() const override; - + bool hasRewardAccumulation() const; + RewardAccumulation const& getRewardAccumulation() const; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; - + + private: + boost::optional rewardAccumulation; }; } }