Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StandardRewardModel.cpp
Go to the documentation of this file.
2
7
9
10namespace storm {
11namespace models {
12namespace sparse {
13template<typename ValueType>
14StandardRewardModel<ValueType>::StandardRewardModel(std::optional<std::vector<ValueType>> const& optionalStateRewardVector,
15 std::optional<std::vector<ValueType>> const& optionalStateActionRewardVector,
16 std::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix)
17 : optionalStateRewardVector(optionalStateRewardVector),
18 optionalStateActionRewardVector(optionalStateActionRewardVector),
19 optionalTransitionRewardMatrix(optionalTransitionRewardMatrix) {
20 // Intentionally left empty.
21}
22
23template<typename ValueType>
24StandardRewardModel<ValueType>::StandardRewardModel(std::optional<std::vector<ValueType>>&& optionalStateRewardVector,
25 std::optional<std::vector<ValueType>>&& optionalStateActionRewardVector,
26 std::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix)
27 : optionalStateRewardVector(std::move(optionalStateRewardVector)),
28 optionalStateActionRewardVector(std::move(optionalStateActionRewardVector)),
29 optionalTransitionRewardMatrix(std::move(optionalTransitionRewardMatrix)) {
30 // Intentionally left empty.
31}
32
33template<typename ValueType>
35 return static_cast<bool>(this->optionalStateRewardVector);
36}
37
38template<typename ValueType>
40 return static_cast<bool>(this->optionalStateRewardVector) && !static_cast<bool>(this->optionalStateActionRewardVector) &&
41 !static_cast<bool>(this->optionalTransitionRewardMatrix);
42}
43
44template<typename ValueType>
45std::vector<ValueType> const& StandardRewardModel<ValueType>::getStateRewardVector() const {
46 STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
47 return this->optionalStateRewardVector.value();
48}
49
50template<typename ValueType>
52 STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
53 return this->optionalStateRewardVector.value();
54}
55
56template<typename ValueType>
57std::optional<std::vector<ValueType>> const& StandardRewardModel<ValueType>::getOptionalStateRewardVector() const {
58 return this->optionalStateRewardVector;
59}
60
61template<typename ValueType>
63 STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
64 STORM_LOG_ASSERT(state < this->optionalStateRewardVector.value().size(), "Invalid state.");
65 return this->optionalStateRewardVector.value()[state];
66}
67
68template<typename ValueType>
69template<typename T>
70void StandardRewardModel<ValueType>::setStateReward(uint_fast64_t state, T const& newReward) {
71 STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
72 STORM_LOG_ASSERT(state < this->optionalStateRewardVector.value().size(), "Invalid state.");
73 this->optionalStateRewardVector.value()[state] = newReward;
74}
75
76template<typename ValueType>
78 return static_cast<bool>(this->optionalStateActionRewardVector);
79}
80
81template<typename ValueType>
83 STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
84 return this->optionalStateActionRewardVector.value();
85}
86
87template<typename ValueType>
89 STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
90 return this->optionalStateActionRewardVector.value();
91}
92
93template<typename ValueType>
94ValueType const& StandardRewardModel<ValueType>::getStateActionReward(uint_fast64_t choiceIndex) const {
95 STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
96 STORM_LOG_ASSERT(choiceIndex < this->optionalStateActionRewardVector.value().size(), "Invalid choiceIndex.");
97 return this->optionalStateActionRewardVector.value()[choiceIndex];
98}
99
100template<typename ValueType>
101template<typename T>
102void StandardRewardModel<ValueType>::setStateActionReward(uint_fast64_t choiceIndex, T const& newValue) {
103 STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
104 STORM_LOG_ASSERT(choiceIndex < this->optionalStateActionRewardVector.value().size(), "Invalid choiceIndex.");
105 this->optionalStateActionRewardVector.value()[choiceIndex] = newValue;
106}
107
108template<typename ValueType>
109std::optional<std::vector<ValueType>> const& StandardRewardModel<ValueType>::getOptionalStateActionRewardVector() const {
110 return this->optionalStateActionRewardVector;
111}
112
113template<typename ValueType>
115 return static_cast<bool>(this->optionalTransitionRewardMatrix);
116}
117
118template<typename ValueType>
120 return this->optionalTransitionRewardMatrix.value();
121}
122
123template<typename ValueType>
125 return this->optionalTransitionRewardMatrix.value();
126}
127
128template<typename ValueType>
129std::optional<storm::storage::SparseMatrix<ValueType>> const& StandardRewardModel<ValueType>::getOptionalTransitionRewardMatrix() const {
130 return this->optionalTransitionRewardMatrix;
131}
132
133template<typename ValueType>
135 std::optional<std::vector<ValueType>> newStateRewardVector(this->getOptionalStateRewardVector());
136 std::optional<std::vector<ValueType>> newStateActionRewardVector;
137 if (this->hasStateActionRewards()) {
138 newStateActionRewardVector = std::vector<ValueType>(enabledActions.getNumberOfSetBits());
139 storm::utility::vector::selectVectorValues(newStateActionRewardVector.value(), enabledActions, this->getStateActionRewardVector());
140 }
141 std::optional<storm::storage::SparseMatrix<ValueType>> newTransitionRewardMatrix;
142 if (this->hasTransitionRewards()) {
143 newTransitionRewardMatrix = this->getTransitionRewardMatrix().restrictRows(enabledActions);
144 }
145 return StandardRewardModel(std::move(newStateRewardVector), std::move(newStateActionRewardVector), std::move(newTransitionRewardMatrix));
146}
147
148template<typename ValueType>
149StandardRewardModel<ValueType> StandardRewardModel<ValueType>::permuteActions(std::vector<uint64_t> const& inversePermutation) const {
150 std::optional<std::vector<ValueType>> newStateRewardVector(this->getOptionalStateRewardVector());
151 std::optional<std::vector<ValueType>> newStateActionRewardVector;
152 if (this->hasStateActionRewards()) {
153 newStateActionRewardVector = storm::utility::vector::applyInversePermutation(inversePermutation, this->getStateActionRewardVector());
154 }
155 std::optional<storm::storage::SparseMatrix<ValueType>> newTransitionRewardMatrix;
156 if (this->hasTransitionRewards()) {
157 newTransitionRewardMatrix = this->getTransitionRewardMatrix().permuteRows(inversePermutation);
158 }
159 return StandardRewardModel(std::move(newStateRewardVector), std::move(newStateActionRewardVector), std::move(newTransitionRewardMatrix));
160}
161
162template<typename ValueType>
164 storm::OptionalRef<std::vector<uint64_t> const> rowGroupIndices,
165 storm::OptionalRef<std::vector<uint64_t> const> permutation) const {
166 std::optional<std::vector<ValueType>> newStateRewardVector;
167 if (hasStateRewards()) {
168 newStateRewardVector = storm::utility::vector::applyInversePermutation(inversePermutation, getStateRewardVector());
169 }
170 std::optional<std::vector<ValueType>> newStateActionRewardVector;
171 if (this->hasStateActionRewards()) {
172 if (rowGroupIndices) {
173 newStateActionRewardVector =
174 storm::utility::vector::applyInversePermutationToGroupedVector(inversePermutation, this->getStateActionRewardVector(), rowGroupIndices.value());
175 } else {
176 STORM_LOG_ASSERT(inversePermutation.size() == this->getStateActionRewardVector().size(), "Invalid permutation size.");
177 newStateActionRewardVector = storm::utility::vector::applyInversePermutation(inversePermutation, this->getStateActionRewardVector());
178 }
179 }
180 std::optional<storm::storage::SparseMatrix<ValueType>> newTransitionRewardMatrix;
181 if (this->hasTransitionRewards()) {
182 STORM_LOG_ASSERT(permutation, "Permutation required for transition rewards.");
183 STORM_LOG_ASSERT(rowGroupIndices.has_value() != getTransitionRewardMatrix().hasTrivialRowGrouping(),
184 "Row group indices required for transition rewards.");
185 this->getTransitionRewardMatrix().permuteRowGroupsAndColumns(inversePermutation, permutation.value());
186 }
187
188 return StandardRewardModel(std::move(newStateRewardVector), std::move(newStateActionRewardVector), std::move(newTransitionRewardMatrix));
189}
190
191template<typename ValueType>
192template<typename MatrixValueType>
194 storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const {
195 ValueType result = this->hasStateActionRewards() ? this->getStateActionReward(choiceIndex) : storm::utility::zero<ValueType>();
196 if (this->hasTransitionRewards()) {
197 result += transitionMatrix.getPointwiseProductRowSum(getTransitionRewardMatrix(), choiceIndex);
198 }
199 return result;
200}
201
202template<typename ValueType>
203template<typename MatrixValueType>
204ValueType StandardRewardModel<ValueType>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex,
205 storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
206 MatrixValueType const& stateRewardWeight, MatrixValueType const& actionRewardWeight) const {
207 ValueType result = actionRewardWeight * getStateActionAndTransitionReward(choiceIndex, transitionMatrix);
208 if (this->hasStateRewards()) {
209 result += stateRewardWeight * this->getStateReward(stateIndex);
210 }
211 return result;
212}
213
214template<typename ValueType>
215template<typename MatrixValueType>
217 std::vector<MatrixValueType> const* weights) {
218 if (this->hasTransitionRewards()) {
219 if (this->hasStateActionRewards()) {
220 storm::utility::vector::addVectors<ValueType>(this->getStateActionRewardVector(),
221 transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()),
222 this->getStateActionRewardVector());
223 this->optionalTransitionRewardMatrix = std::nullopt;
224 } else {
225 this->optionalStateActionRewardVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
226 }
227 }
228
229 if (reduceToStateRewards && this->hasStateActionRewards()) {
230 STORM_LOG_THROW(transitionMatrix.getRowGroupCount() == this->getStateActionRewardVector().size(), storm::exceptions::InvalidOperationException,
231 "The reduction to state rewards is only possible if the size of the action reward vector equals the number of states.");
232 if (weights) {
233 if (this->hasStateRewards()) {
234 storm::utility::vector::applyPointwiseTernary<ValueType, MatrixValueType, ValueType>(
235 this->getStateActionRewardVector(), *weights, this->getStateRewardVector(),
236 [](ValueType const& sar, MatrixValueType const& w, ValueType const& sr) -> ValueType { return sr + w * sar; });
237 } else {
238 this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector);
239 storm::utility::vector::applyPointwise<ValueType, MatrixValueType, ValueType, std::multiplies<>>(
240 this->optionalStateRewardVector.value(), *weights, this->optionalStateRewardVector.value());
241 }
242 } else {
243 if (this->hasStateRewards()) {
244 storm::utility::vector::addVectors<ValueType>(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector());
245 } else {
246 this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector);
247 }
248 }
249 this->optionalStateActionRewardVector = std::nullopt;
250 }
251}
252
253template<typename ValueType>
254template<typename MatrixValueType>
256 std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix())
257 : (this->hasStateActionRewards() ? this->getStateActionRewardVector()
258 : std::vector<ValueType>(transitionMatrix.getRowCount()));
259 if (this->hasStateActionRewards() && this->hasTransitionRewards()) {
260 storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result);
261 }
262 if (this->hasStateRewards()) {
263 storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), transitionMatrix.getRowGroupIndices());
264 }
265 return result;
266}
267
268template<typename ValueType>
269template<typename MatrixValueType>
271 std::vector<MatrixValueType> const& weights) const {
272 std::vector<ValueType> result;
273 if (this->hasTransitionRewards()) {
274 result = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
275 storm::utility::vector::applyPointwiseTernary<MatrixValueType, ValueType, ValueType>(
276 weights, this->getStateActionRewardVector(), result,
277 [](MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) {
278 return weight * (resultElement + rewardElement);
279 });
280 } else {
281 result = std::vector<ValueType>(transitionMatrix.getRowCount());
282 if (this->hasStateActionRewards()) {
283 storm::utility::vector::applyPointwise<MatrixValueType, ValueType, ValueType>(
284 weights, this->getStateActionRewardVector(), result,
285 [](MatrixValueType const& weight, ValueType const& rewardElement) { return weight * rewardElement; });
286 }
287 }
288 if (this->hasStateRewards()) {
289 storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), transitionMatrix.getRowGroupIndices());
290 }
291 return result;
292}
293
294template<typename ValueType>
295template<typename MatrixValueType>
296std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(uint_fast64_t numberOfRows,
297 storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
298 storm::storage::BitVector const& filter) const {
299 std::vector<ValueType> result(numberOfRows);
300 if (this->hasTransitionRewards()) {
301 std::vector<ValueType> pointwiseProductRowSumVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
302 storm::utility::vector::selectVectorValues(result, filter, transitionMatrix.getRowGroupIndices(), pointwiseProductRowSumVector);
303 }
304
305 if (this->hasStateActionRewards()) {
306 storm::utility::vector::addFilteredVectorGroupsToGroupedVector(result, this->getStateActionRewardVector(), filter,
307 transitionMatrix.getRowGroupIndices());
308 }
309 if (this->hasStateRewards()) {
310 storm::utility::vector::addFilteredVectorToGroupedVector(result, this->getStateRewardVector(), filter, transitionMatrix.getRowGroupIndices());
311 }
312 return result;
313}
314
315template<typename ValueType>
316template<typename MatrixValueType>
318 std::vector<MatrixValueType> const& stateRewardWeights) const {
319 std::vector<ValueType> result;
320 if (this->hasTransitionRewards()) {
321 result = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
322 } else {
323 result = std::vector<ValueType>(transitionMatrix.getRowCount());
324 }
325 if (this->hasStateActionRewards()) {
326 storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result);
327 }
328 if (this->hasStateRewards()) {
329 std::vector<ValueType> scaledStateRewardVector(transitionMatrix.getRowGroupCount());
330 storm::utility::vector::multiplyVectorsPointwise(this->getStateRewardVector(), stateRewardWeights, scaledStateRewardVector);
331 storm::utility::vector::addVectorToGroupedVector(result, scaledStateRewardVector, transitionMatrix.getRowGroupIndices());
332 }
333 return result;
334}
335
336template<typename ValueType>
337template<typename MatrixValueType>
339 return getStatesWithFilter(transitionMatrix, storm::utility::isZero<ValueType>);
340}
341
342template<typename ValueType>
343template<typename MatrixValueType>
345 std::function<bool(ValueType const&)> const& filter) const {
346 storm::storage::BitVector result = this->hasStateRewards() ? storm::utility::vector::filter(this->getStateRewardVector(), filter)
347 : storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true);
348 if (this->hasStateActionRewards()) {
349 for (uint_fast64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) {
350 for (uint_fast64_t row = transitionMatrix.getRowGroupIndices()[state]; row < transitionMatrix.getRowGroupIndices()[state + 1]; ++row) {
351 if (!filter(this->getStateActionRewardVector()[row])) {
352 result.set(state, false);
353 break;
354 }
355 }
356 }
357 }
358 if (this->hasTransitionRewards()) {
359 for (uint_fast64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) {
360 for (auto const& rewardMatrixEntry : this->getTransitionRewardMatrix().getRowGroup(state)) {
361 if (!filter(rewardMatrixEntry.getValue())) {
362 result.set(state, false);
363 break;
364 }
365 }
366 }
367 }
368 return result;
369}
370
371template<typename ValueType>
372template<typename MatrixValueType>
374 storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const {
375 return getChoicesWithFilter(transitionMatrix, storm::utility::isZero<ValueType>);
376}
377
378template<typename ValueType>
379template<typename MatrixValueType>
381 std::function<bool(ValueType const&)> const& filter) const {
383 if (this->hasStateActionRewards()) {
384 result = storm::utility::vector::filter(this->getStateActionRewardVector(), filter);
385 if (this->hasStateRewards()) {
386 result &= transitionMatrix.getRowFilter(storm::utility::vector::filter(this->getStateRewardVector(), filter));
387 }
388 } else {
389 if (this->hasStateRewards()) {
390 result = transitionMatrix.getRowFilter(storm::utility::vector::filter(this->getStateRewardVector(), filter));
391 } else {
392 result = storm::storage::BitVector(transitionMatrix.getRowCount(), true);
393 }
394 }
395 if (this->hasTransitionRewards()) {
396 for (uint_fast64_t row = 0; row < transitionMatrix.getRowCount(); ++row) {
397 for (auto const& rewardMatrixEntry : this->getTransitionRewardMatrix().getRow(row)) {
398 if (!filter(rewardMatrixEntry.getValue())) {
399 result.set(row, false);
400 break;
401 }
402 }
403 }
404 }
405 return result;
406}
407
408template<typename ValueType>
409template<typename MatrixValueType>
411 if (hasStateRewards()) {
412 getStateRewardVector()[state] = storm::utility::zero<ValueType>();
413 }
414 if (hasStateActionRewards()) {
415 for (uint_fast64_t choice = transitions.getRowGroupIndices()[state]; choice < transitions.getRowGroupIndices()[state + 1]; ++choice) {
416 getStateActionRewardVector()[choice] = storm::utility::zero<ValueType>();
417 }
418 }
419 if (hasTransitionRewards()) {
420 for (auto& entry : getTransitionRewardMatrix().getRowGroup(state)) {
421 entry.setValue(storm::utility::zero<ValueType>());
422 }
423 }
424}
425
426template<typename ValueType>
428 return !(static_cast<bool>(this->optionalStateRewardVector) || static_cast<bool>(this->optionalStateActionRewardVector) ||
429 static_cast<bool>(this->optionalTransitionRewardMatrix));
430}
431
435template<typename ValueType>
436bool anyOfRewardValues(StandardRewardModel<ValueType> const& rewardModel, auto const& predicate) {
437 if (rewardModel.hasStateRewards() && std::any_of(rewardModel.getStateRewardVector().begin(), rewardModel.getStateRewardVector().end(), predicate)) {
438 return true;
439 }
440 if (rewardModel.hasStateActionRewards() &&
441 std::any_of(rewardModel.getStateActionRewardVector().begin(), rewardModel.getStateActionRewardVector().end(), predicate)) {
442 return true;
443 }
444 if (rewardModel.hasTransitionRewards()) {
445 for (auto const& entry : rewardModel.getTransitionRewardMatrix()) {
446 if (predicate(entry.getValue())) {
447 return true;
448 }
449 }
450 }
451 return false;
452}
453
454template<typename ValueType>
456 bool const hasNonZeroReward = anyOfRewardValues(*this, [](auto&& value) { return !storm::utility::isZero<ValueType>(value); });
457 return !hasNonZeroReward;
458}
459
460template<typename ValueType>
462 if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
463 // Rational functions can never be negative.
464 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Checking Rational functions for negativity is not possible.");
465 return false;
466 } else {
467 return anyOfRewardValues(*this, [](auto&& value) { return value < storm::utility::zero<ValueType>(); });
468 }
469}
470
471template<typename ValueType>
473 if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
474 // Rational functions can never be negative.
475 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Checking Rational functions for negativity is not possible.");
476 return false;
477 } else {
478 return anyOfRewardValues(*this, [](auto&& value) { return value > storm::utility::zero<ValueType>(); });
479 }
480}
481
482template<typename ValueType>
483bool StandardRewardModel<ValueType>::isCompatible(uint_fast64_t nrStates, uint_fast64_t nrChoices) const {
484 if (hasStateRewards()) {
485 if (optionalStateRewardVector.value().size() != nrStates)
486 return false;
487 }
488 if (hasStateActionRewards()) {
489 if (optionalStateActionRewardVector.value().size() != nrChoices)
490 return false;
491 }
492 return true;
493}
494
495template<typename ValueType>
497 size_t seed = 0;
498 if (hasStateRewards()) {
499 boost::hash_combine(seed, boost::hash_range(optionalStateRewardVector->begin(), optionalStateRewardVector->end()));
500 }
501 if (hasStateActionRewards()) {
502 boost::hash_combine(seed, boost::hash_range(optionalStateActionRewardVector->begin(), optionalStateActionRewardVector->end()));
503 }
504 if (hasTransitionRewards()) {
505 boost::hash_combine(seed, optionalTransitionRewardMatrix->hash());
506 }
507 return seed;
508}
509
510template<typename ValueType>
511std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueType> const& rewardModel) {
512 out << std::boolalpha << "reward model [state reward: " << rewardModel.hasStateRewards()
513 << ", state-action rewards: " << rewardModel.hasStateActionRewards() << ", transition rewards: " << rewardModel.hasTransitionRewards() << "]"
514 << std::noboolalpha;
515 return out;
516}
517
518std::set<storm::RationalFunctionVariable> getRewardModelParameters(StandardRewardModel<storm::RationalFunction> const& rewModel) {
519 std::set<storm::RationalFunctionVariable> vars;
520 if (rewModel.hasTransitionRewards()) {
521 vars = storm::storage::getVariables(rewModel.getTransitionRewardMatrix());
522 }
523 if (rewModel.hasStateActionRewards()) {
524 std::set<storm::RationalFunctionVariable> tmp = storm::utility::vector::getVariables(rewModel.getStateActionRewardVector());
525 vars.insert(tmp.begin(), tmp.end());
526 }
527 if (rewModel.hasStateRewards()) {
528 std::set<storm::RationalFunctionVariable> tmp = storm::utility::vector::getVariables(rewModel.getStateRewardVector());
529 vars.insert(tmp.begin(), tmp.end());
530 }
531 return vars;
532}
533
534// Explicitly instantiate the class.
535template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
536template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(uint_fast64_t numberOfRows,
537 storm::storage::SparseMatrix<double> const& transitionMatrix,
538 storm::storage::BitVector const& filter) const;
539template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix,
540 std::vector<double> const& weights) const;
542 std::vector<double> const& stateRewardWeights) const;
545 std::function<bool(double const&)> const& filter) const;
548 std::function<bool(double const&)> const& filter) const;
549template double StandardRewardModel<double>::getStateActionAndTransitionReward(uint_fast64_t stateIndex,
550 storm::storage::SparseMatrix<double> const& transitionMatrix) const;
551template double StandardRewardModel<double>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex,
552 storm::storage::SparseMatrix<double> const& transitionMatrix,
553 double const& stateRewardWeight, double const& actionRewardWeight) const;
554template void StandardRewardModel<double>::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix<double> const& transitionMatrix);
555template void StandardRewardModel<double>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards,
556 std::vector<double> const* weights);
557template void StandardRewardModel<double>::setStateActionReward(uint_fast64_t choiceIndex, double const& newValue);
558template void StandardRewardModel<double>::setStateReward(uint_fast64_t state, double const& newValue);
559template class StandardRewardModel<double>;
560template std::ostream& operator<< <double>(std::ostream& out, StandardRewardModel<double> const& rewardModel);
561
562#ifdef STORM_HAVE_CARL
563template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(
564 uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& filter) const;
565template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(
566 storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
567template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(
568 storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& weights) const;
569template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalActionRewardVector(
570 storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& stateRewardWeights) const;
572 storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
574 storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::function<bool(storm::RationalNumber const&)> const& filter) const;
576 storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
578 storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::function<bool(storm::RationalNumber const&)> const& filter) const;
580 uint_fast64_t stateIndex, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
582 uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix,
583 storm::RationalNumber const& stateRewardWeight, storm::RationalNumber const& actionRewardWeight) const;
585 bool reduceToStateRewards,
586 std::vector<storm::RationalNumber> const* weights);
589template void StandardRewardModel<storm::RationalNumber>::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const& newValue);
590template void StandardRewardModel<storm::RationalNumber>::setStateReward(uint_fast64_t state, storm::RationalNumber const& newValue);
592template std::ostream& operator<< <storm::RationalNumber>(std::ostream& out, StandardRewardModel<storm::RationalNumber> const& rewardModel);
593
594template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(
595 uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& filter) const;
596template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(
597 storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
598template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(
599 storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& weights) const;
601 storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
603 storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::function<bool(storm::RationalFunction const&)> const& filter) const;
605 storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
607 storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::function<bool(storm::RationalFunction const&)> const& filter) const;
610template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalActionRewardVector(
611 storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& stateRewardWeights) const;
613 uint_fast64_t stateIndex, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
615 uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix,
616 storm::RationalFunction const& stateRewardWeight, storm::RationalFunction const& actionRewardWeight) const;
618 storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, bool reduceToStateRewards,
619 std::vector<storm::RationalFunction> const* weights);
620template void StandardRewardModel<storm::RationalFunction>::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalFunction const& newValue);
621template void StandardRewardModel<storm::RationalFunction>::setStateReward(uint_fast64_t state, storm::RationalFunction const& newValue);
623template std::ostream& operator<< <storm::RationalFunction>(std::ostream& out, StandardRewardModel<storm::RationalFunction> const& rewardModel);
624
625template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(uint_fast64_t numberOfRows,
626 storm::storage::SparseMatrix<double> const& transitionMatrix,
627 storm::storage::BitVector const& filter) const;
628template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(
629 storm::storage::SparseMatrix<double> const& transitionMatrix) const;
630template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix,
631 std::vector<double> const& weights) const;
632template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(
633 uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix, storm::storage::BitVector const& filter) const;
634template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(
635 storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix) const;
636template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(
637 storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix, std::vector<storm::Interval> const& weights) const;
638template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalActionRewardVector(
639 storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& stateRewardWeights) const;
641 std::function<bool(storm::Interval const&)> const& filter) const;
643 storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix, std::function<bool(storm::Interval const&)> const& filter) const;
645 std::function<bool(storm::Interval const&)> const& filter) const;
647 storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix, std::function<bool(storm::Interval const&)> const& filter) const;
648template void StandardRewardModel<storm::Interval>::setStateActionReward(uint_fast64_t choiceIndex, double const& newValue);
649template void StandardRewardModel<storm::Interval>::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const& newValue);
650template void StandardRewardModel<storm::Interval>::setStateReward(uint_fast64_t state, double const& newValue);
651template void StandardRewardModel<storm::Interval>::setStateReward(uint_fast64_t state, storm::Interval const& newValue);
652template void StandardRewardModel<storm::Interval>::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix<double> const& transitionMatrix);
653template void StandardRewardModel<storm::Interval>::clearRewardAtState(uint_fast64_t state,
654 storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix);
656 bool reduceToStateRewards, std::vector<double> const* weights);
658 bool reduceToStateRewards, std::vector<storm::Interval> const* weights);
660 storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix) const;
662 storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix) const;
664template std::ostream& operator<< <storm::Interval>(std::ostream& out, StandardRewardModel<storm::Interval> const& rewardModel);
665#endif
666} // namespace sparse
667
668} // namespace models
669} // namespace storm
Helper class that optionally holds a reference to an object of type T.
Definition OptionalRef.h:48
storm::storage::SparseMatrix< ValueType > const & getTransitionRewardMatrix() const
Retrieves the transition rewards of the reward model.
bool hasTransitionRewards() const
Retrieves whether the reward model has transition rewards.
StandardRewardModel< ValueType > restrictActions(storm::storage::BitVector const &enabledActions) const
Creates a new reward model by restricting the actions of the action-based rewards.
std::optional< storm::storage::SparseMatrix< ValueType > > const & getOptionalTransitionRewardMatrix() const
Retrieves an optional value that contains the transition reward matrix if there is one.
void setStateReward(uint_fast64_t state, T const &newReward)
bool hasOnlyStateRewards() const
Retrieves whether the reward model only has state rewards (and hence no other rewards).
std::vector< ValueType > getTotalActionRewardVector(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix, std::vector< MatrixValueType > const &stateRewardWeights) const
Creates a vector representing the complete action-based rewards, i.e., state-action- and transition-b...
ValueType const & getStateReward(uint_fast64_t state) const
std::optional< std::vector< ValueType > > const & getOptionalStateRewardVector() const
Retrieves an optional value that contains the state reward vector if there is one.
std::vector< ValueType > const & getStateActionRewardVector() const
Retrieves the state-action rewards of the reward model.
std::vector< ValueType > const & getStateRewardVector() const
Retrieves the state rewards of the reward model.
storm::storage::BitVector getStatesWithZeroReward(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix) const
Returns the set of states at which a all rewards (state-, action- and transition-rewards) are zero.
void clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix< MatrixValueType > const &transitions)
Sets all available rewards at this state to zero.
ValueType const & getStateActionReward(uint_fast64_t choiceIndex) const
Retrieves the state-action reward for the given choice.
bool empty() const
Retrieves whether the reward model is empty, i.e.
ValueType getStateActionAndTransitionReward(uint_fast64_t choiceIndex, storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix) const
bool isCompatible(uint_fast64_t nrStates, uint_fast64_t nrChoices) const
Checks whether the reward model is compatible with key model characteristics.
std::vector< ValueType > getTotalRewardVector(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix) const
Creates a vector representing the complete reward vector based on the state-, state-action- and trans...
void reduceToStateBasedRewards(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix, bool reduceToStateRewards=false, std::vector< MatrixValueType > const *weights=nullptr)
Reduces the transition-based rewards to state-action rewards by taking the average of each row.
ValueType getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix, MatrixValueType const &stateRewardWeight=storm::utility::one< MatrixValueType >(), MatrixValueType const &actionRewardWeight=storm::utility::one< MatrixValueType >()) const
Retrieves the total reward for the given state action pair (including (scaled) state rewards,...
StandardRewardModel(std::optional< std::vector< ValueType > > const &optionalStateRewardVector=std::nullopt, std::optional< std::vector< ValueType > > const &optionalStateActionRewardVector=std::nullopt, std::optional< storm::storage::SparseMatrix< ValueType > > const &optionalTransitionRewardMatrix=std::nullopt)
Constructs a reward model by copying the given data.
bool hasStateRewards() const
Retrieves whether the reward model has state rewards.
bool hasStateActionRewards() const
Retrieves whether the reward model has state-action rewards.
storm::storage::BitVector getChoicesWithZeroReward(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix) const
Returns the set of choices at which all rewards (state-, action- and transition-rewards) are zero.
bool isAllZero() const
Retrieves whether every reward defined by this reward model is zero.
storm::storage::BitVector getChoicesWithFilter(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix, std::function< bool(ValueType const &)> const &filter) const
Returns the set of choices for which all associated rewards (state, action or transition rewards) sat...
void setStateActionReward(uint_fast64_t choiceIndex, T const &newValue)
Sets the state-action reward for the given choice.
storm::storage::BitVector getStatesWithFilter(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix, std::function< bool(ValueType const &)> const &filter) const
Returns the set of states for which all associated rewards (state, action or transition rewards) sati...
StandardRewardModel< ValueType > permuteActions(std::vector< uint64_t > const &inversePermutation) const
Creates a new reward model by permuting the actions.
StandardRewardModel< ValueType > permuteStates(std::vector< uint64_t > const &inversePermutation, storm::OptionalRef< std::vector< uint64_t > const > rowGroupIndices=storm::NullRef, storm::OptionalRef< std::vector< uint64_t > const > permutation=storm::NullRef) const
Creates a new reward model by permuting the states.
std::optional< std::vector< ValueType > > const & getOptionalStateActionRewardVector() const
Retrieves an optional value that contains the state-action reward vector if there is one.
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
void set(uint_fast64_t index, bool value=true)
Sets the given truth value at the given index.
uint_fast64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
A class that holds a possibly non-square matrix in the compressed row storage format.
std::vector< ResultValueType > getPointwiseProductRowSumVector(storm::storage::SparseMatrix< OtherValueType > const &otherMatrix) const
Performs a pointwise matrix multiplication of the matrix with the given matrix and returns a vector c...
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
ResultValueType getPointwiseProductRowSum(storm::storage::SparseMatrix< OtherValueType > const &otherMatrix, index_type const &row) const
Performs a pointwise multiplication of the entries in the given row of this matrix and the entries of...
std::vector< index_type > const & getRowGroupIndices() const
Returns the grouping of rows of this matrix.
index_type getRowCount() const
Returns the number of rows of the matrix.
storm::storage::BitVector getRowFilter(storm::storage::BitVector const &groupConstraint) const
Returns a bitvector representing the set of rows, with all indices set that correspond to one of the ...
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::set< storm::RationalFunctionVariable > getRewardModelParameters(StandardRewardModel< storm::RationalFunction > const &rewModel)
template std::ostream & operator<<< double >(std::ostream &out, StandardRewardModel< double > const &rewardModel)
std::ostream & operator<<(std::ostream &out, ChoiceLabeling const &labeling)
bool anyOfRewardValues(StandardRewardModel< ValueType > const &rewardModel, auto const &predicate)
Auxiliary function to check if the given predicate is true for any of the reward values in the given ...
storm::storage::BitVector filter(std::vector< T > const &values, std::function< bool(T const &value)> const &function)
Retrieves a bit vector containing all the indices for which the value at this position makes the give...
Definition vector.h:490
void addVectors(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target)
Adds the two given vectors and writes the result to the target vector.
Definition vector.h:403
void addVectorToGroupedVector(std::vector< T > &target, std::vector< T > const &source, std::vector< uint_fast64_t > const &rowGroupIndices)
Adds the source vector to the target vector in a way such that the i-th entry is added to all element...
Definition vector.h:309
void addFilteredVectorGroupsToGroupedVector(std::vector< T > &target, std::vector< T > const &source, storm::storage::BitVector const &filter, std::vector< uint_fast64_t > const &rowGroupIndices)
Definition vector.h:288
void selectVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Selects the elements from a vector at the specified positions and writes them consecutively into anot...
Definition vector.h:188
void multiplyVectorsPointwise(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target)
Multiplies the two given vectors (pointwise) and writes the result to the target vector.
Definition vector.h:427
void addFilteredVectorToGroupedVector(std::vector< T > &target, std::vector< T > const &source, storm::storage::BitVector const &filter, std::vector< uint_fast64_t > const &rowGroupIndices)
Adds the source vector to the target vector in a way such that the i-th selected entry is added to al...
Definition vector.h:334
std::vector< T > applyInversePermutation(std::vector< uint64_t > const &inversePermutation, std::vector< T > const &source)
Definition vector.h:1118
std::set< storm::RationalFunctionVariable > getVariables(std::vector< storm::RationalFunction > const &vector)
std::vector< T > applyInversePermutationToGroupedVector(std::vector< uint64_t > const &inversePermutation, std::vector< T > const &source, std::vector< uint64_t > const &rowGroupIndices)
Definition vector.h:1128
LabParser.cpp.
Definition cli.cpp:18