Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
CumulativeRewardFormula.cpp
Go to the documentation of this file.
1
3#include <boost/any.hpp>
4#include <ostream>
5
8
13
14namespace storm {
15namespace logic {
17 boost::optional<RewardAccumulation> rewardAccumulation)
18 : timeBoundReferences({timeBoundReference}), bounds({bound}), rewardAccumulation(rewardAccumulation) {
19 // Intentionally left empty.
20}
21
22CumulativeRewardFormula::CumulativeRewardFormula(std::vector<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences,
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.");
27}
28
30 return true;
31}
32
34 return true;
35}
36
40
42 return timeBoundReferences.size();
43}
44
45boost::any CumulativeRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
46 return visitor.visit(*this, data);
47}
48
49void CumulativeRewardFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
50 for (unsigned i = 0; i < this->getDimension(); ++i) {
52 referencedRewardModels.insert(this->getTimeBoundReference(i).getRewardName());
53 }
54 }
55}
56
57void CumulativeRewardFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
58 for (unsigned i = 0; i < this->getDimension(); ++i) {
59 this->getBound(i).gatherVariables(usedVariables);
60 }
61}
62
64 STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
65 return getTimeBoundReference(0);
66}
67
69 return timeBoundReferences.at(i);
70}
71
73 STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
74 return isBoundStrict(0);
75}
76
78 return bounds.at(i).isStrict();
79}
80
82 STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
83 return hasIntegerBound(0);
84}
85
87 return bounds.at(i).getBound().hasIntegerType();
88}
89
91 STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
92 return getBound(0);
93}
94
96 return bounds.at(i).getBound();
97}
98
99template<typename ValueType>
101 STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
102 return getBound<ValueType>(0);
103}
104
105template<>
106double CumulativeRewardFormula::getBound(unsigned i) const {
107 checkNoVariablesInBound(bounds.at(i).getBound());
108 double value = bounds.at(i).getBound().evaluateAsDouble();
109 return value;
110}
111
112template<>
113storm::RationalNumber CumulativeRewardFormula::getBound(unsigned i) const {
114 checkNoVariablesInBound(bounds.at(i).getBound());
115 storm::RationalNumber value = bounds.at(i).getBound().evaluateAsRational();
116 return value;
117}
118
119template<>
120uint64_t CumulativeRewardFormula::getBound(unsigned i) const {
121 checkNoVariablesInBound(bounds.at(i).getBound());
122 uint64_t value = bounds.at(i).getBound().evaluateAsInt();
123 return value;
124}
125
126template<>
128 STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
129 double bound = getBound<double>();
130 STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
131 return bound;
132}
133
134template<>
136 STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
137 int_fast64_t bound = getBound<uint64_t>();
138 if (isBoundStrict()) {
139 STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
140 return bound - 1;
141 } else {
142 return bound;
143 }
144}
145
146std::vector<TimeBound> const& CumulativeRewardFormula::getBounds() const {
147 return bounds;
148}
149
150void CumulativeRewardFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) {
151 STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException,
152 "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants.");
153}
154
156 return rewardAccumulation.is_initialized();
157}
158
160 return rewardAccumulation.get();
161}
162
163std::shared_ptr<CumulativeRewardFormula const> CumulativeRewardFormula::stripRewardAccumulation() const {
164 return std::make_shared<CumulativeRewardFormula const>(bounds, timeBoundReferences);
165}
166
167std::shared_ptr<CumulativeRewardFormula const> CumulativeRewardFormula::restrictToDimension(unsigned i) const {
168 return std::make_shared<CumulativeRewardFormula const>(bounds.at(i), getTimeBoundReference(i), rewardAccumulation);
169}
170
171std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out, bool /*allowParentheses*/) const {
172 // No parentheses necessary
173 out << "C";
174 if (hasRewardAccumulation()) {
175 out << "[" << getRewardAccumulation() << "]";
176 }
177 if (this->isMultiDimensional()) {
178 out << "^{";
179 }
180 for (unsigned i = 0; i < this->getDimension(); ++i) {
181 if (i > 0) {
182 out << ", ";
183 }
184 if (this->getTimeBoundReference(i).isRewardBound()) {
185 out << "rew";
187 out << "[" << this->getTimeBoundReference(i).getRewardAccumulation() << "]";
188 }
189 out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}";
190 } else if (this->getTimeBoundReference(i).isStepBound()) {
191 out << "steps";
192 //} else if (this->getTimeBoundReference(i).isStepBound())
193 // Note: the 'time' keyword is optional.
194 // out << "time";
195 }
196 if (this->isBoundStrict(i)) {
197 out << "<";
198 } else {
199 out << "<=";
200 }
201 out << this->getBound(i);
202 }
203 if (this->isMultiDimensional()) {
204 out << "}";
205 }
206 return out;
207}
208
209template uint64_t CumulativeRewardFormula::getBound<uint64_t>() const;
210template double CumulativeRewardFormula::getBound<double>() const;
211template storm::RationalNumber CumulativeRewardFormula::getBound<storm::RationalNumber>() const;
212
213} // namespace logic
214} // namespace storm
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.
TimeBoundReference const & getTimeBoundReference() const
std::shared_ptr< CumulativeRewardFormula const > stripRewardAccumulation() const
RewardAccumulation const & getRewardAccumulation() const
std::vector< TimeBound > const & getBounds() const
std::shared_ptr< CumulativeRewardFormula const > restrictToDimension(unsigned i) const
virtual bool isRewardPathFormula() const override
virtual void gatherReferencedRewardModels(std::set< std::string > &referencedRewardModels) const override
virtual void gatherUsedVariables(std::set< storm::expressions::Variable > &usedVariables) const override
storm::expressions::Expression const & getBound() const
virtual boost::any accept(FormulaVisitor const &visitor, boost::any const &data) const override
virtual std::ostream & writeToStream(std::ostream &out, bool allowParentheses=false) const override
Writes the forumla to the given output stream.
virtual bool isCumulativeRewardFormula() const override
CumulativeRewardFormula(TimeBound const &bound, TimeBoundReference const &timeBoundReference=TimeBoundReference(TimeBoundType::Time), boost::optional< RewardAccumulation > rewardAccumulation=boost::none)
virtual boost::any visit(AtomicExpressionFormula const &f, boost::any const &data) const =0
std::string const & getRewardName() const
RewardAccumulation const & getRewardAccumulation() const
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
LabParser.cpp.
Definition cli.cpp:18