3#include <boost/any.hpp>
17 boost::optional<RewardAccumulation> rewardAccumulation)
18 : timeBoundReferences({timeBoundReference}), bounds({bound}), rewardAccumulation(rewardAccumulation) {
23 boost::optional<RewardAccumulation> rewardAccumulation)
24 : timeBoundReferences(timeBoundReferences), bounds(bounds), rewardAccumulation(rewardAccumulation) {
25 STORM_LOG_ASSERT(this->timeBoundReferences.size() == this->bounds.size(),
"Number of time bounds and number of time bound references does not match.");
26 STORM_LOG_ASSERT(!this->timeBoundReferences.empty(),
"No time bounds given.");
42 return timeBoundReferences.size();
46 return visitor.
visit(*
this, data);
69 return timeBoundReferences.at(i);
78 return bounds.at(i).isStrict();
87 return bounds.at(i).getBound().hasIntegerType();
96 return bounds.at(i).getBound();
99template<
typename ValueType>
102 return getBound<ValueType>(0);
107 checkNoVariablesInBound(bounds.at(i).getBound());
108 double value = bounds.at(i).getBound().evaluateAsDouble();
114 checkNoVariablesInBound(bounds.at(i).getBound());
115 storm::RationalNumber value = bounds.at(i).getBound().evaluateAsRational();
121 checkNoVariablesInBound(bounds.at(i).getBound());
122 uint64_t value = bounds.at(i).getBound().evaluateAsInt();
129 double bound = getBound<double>();
130 STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException,
"Cannot retrieve non-strict bound from strict zero-bound.");
137 int_fast64_t bound = getBound<uint64_t>();
139 STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException,
"Cannot retrieve non-strict bound from strict zero-bound.");
152 "Cannot evaluate time-bound '" << bound <<
"' as it contains undefined constants.");
156 return rewardAccumulation.is_initialized();
160 return rewardAccumulation.get();
164 return std::make_shared<CumulativeRewardFormula const>(bounds, timeBoundReferences);
168 return std::make_shared<CumulativeRewardFormula const>(bounds.at(i),
getTimeBoundReference(i), rewardAccumulation);
209template uint64_t CumulativeRewardFormula::getBound<uint64_t>()
const;
210template double CumulativeRewardFormula::getBound<double>()
const;
211template storm::RationalNumber CumulativeRewardFormula::getBound<storm::RationalNumber>()
const;
bool containsVariables() const
Retrieves whether the expression contains a variable.
void gatherVariables(std::set< storm::expressions::Variable > &variables) const
Retrieves the set of all variables that appear in the expression.
std::string const & getRewardName() const
bool isRewardBound() const
RewardAccumulation const & getRewardAccumulation() const
bool hasRewardAccumulation() const
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)