Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StandardRewardModel.h
Go to the documentation of this file.
1#pragma once
2
3#include <optional>
4#include <set>
5#include <vector>
6
11
12namespace storm {
13namespace models {
14namespace sparse {
15template<typename CValueType>
17 public:
18 typedef CValueType ValueType;
19
27 StandardRewardModel(std::optional<std::vector<ValueType>> const& optionalStateRewardVector = std::nullopt,
28 std::optional<std::vector<ValueType>> const& optionalStateActionRewardVector = std::nullopt,
29 std::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix = std::nullopt);
30
38 StandardRewardModel(std::optional<std::vector<ValueType>>&& optionalStateRewardVector,
39 std::optional<std::vector<ValueType>>&& optionalStateActionRewardVector = std::nullopt,
40 std::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix = std::nullopt);
41
44
47
53 bool hasStateRewards() const;
54
60 bool hasOnlyStateRewards() const;
61
68 std::vector<ValueType> const& getStateRewardVector() const;
69
76 std::vector<ValueType>& getStateRewardVector();
77
78 ValueType const& getStateReward(uint_fast64_t state) const;
79
80 template<typename T>
81 void setStateReward(uint_fast64_t state, T const& newReward);
82
83 // template<typename T=ValueType, EnableIf<hasTotalOrder<T>>>
84 // ValueType maximalStateReward(uint_fast64_t state) const;
85
91 std::optional<std::vector<ValueType>> const& getOptionalStateRewardVector() const;
92
98 bool hasStateActionRewards() const;
99
106 std::vector<ValueType> const& getStateActionRewardVector() const;
107
114 std::vector<ValueType>& getStateActionRewardVector();
115
119 ValueType const& getStateActionReward(uint_fast64_t choiceIndex) const;
120
124 template<typename T>
125 void setStateActionReward(uint_fast64_t choiceIndex, T const& newValue);
126
130 template<typename MatrixValueType>
131 void clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix<MatrixValueType> const& transitions);
132
138 std::optional<std::vector<ValueType>> const& getOptionalStateActionRewardVector() const;
139
145 bool hasTransitionRewards() const;
146
154
162
168 std::optional<storm::storage::SparseMatrix<ValueType>> const& getOptionalTransitionRewardMatrix() const;
169
176 template<typename MatrixValueType>
177 ValueType getStateActionAndTransitionReward(uint_fast64_t choiceIndex, storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const;
178
189 template<typename MatrixValueType>
190 ValueType getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex,
191 storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
192 MatrixValueType const& stateRewardWeight = storm::utility::one<MatrixValueType>(),
193 MatrixValueType const& actionRewardWeight = storm::utility::one<MatrixValueType>()) const;
194
202
208 StandardRewardModel<ValueType> permuteActions(std::vector<uint64_t> const& inversePermutation) const;
209
217 StandardRewardModel<ValueType> permuteStates(std::vector<uint64_t> const& inversePermutation,
218 storm::OptionalRef<std::vector<uint64_t> const> rowGroupIndices = storm::NullRef,
219 storm::OptionalRef<std::vector<uint64_t> const> permutation = storm::NullRef) const;
220
233 template<typename MatrixValueType>
234 void reduceToStateBasedRewards(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, bool reduceToStateRewards = false,
235 std::vector<MatrixValueType> const* weights = nullptr);
236
244 template<typename MatrixValueType>
245 std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const;
246
255 template<typename MatrixValueType>
256 std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
257 std::vector<MatrixValueType> const& weights) const;
258
268 template<typename MatrixValueType>
269 std::vector<ValueType> getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
270 storm::storage::BitVector const& filter) const;
271
281 template<typename MatrixValueType>
282 std::vector<ValueType> getTotalActionRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
283 std::vector<MatrixValueType> const& stateRewardWeights) const;
284
291 template<typename MatrixValueType>
293
298 template<typename MatrixValueType>
300 std::function<bool(ValueType const&)> const& filter) const;
301
308 template<typename MatrixValueType>
310
315 template<typename MatrixValueType>
317 std::function<bool(ValueType const&)> const& filter) const;
318
325 bool empty() const;
326
332 bool isAllZero() const;
333
337 bool hasNegativeRewards() const;
338
342 bool hasPositiveRewards() const;
343
354 bool isCompatible(uint_fast64_t nrStates, uint_fast64_t nrChoices) const;
355
356 std::size_t hash() const;
357
358 template<typename ValueTypePrime>
359 friend std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueTypePrime> const& rewardModel);
360
361 private:
362 // An (optional) vector representing the state rewards.
363 std::optional<std::vector<ValueType>> optionalStateRewardVector;
364
365 // An (optional) vector representing the state-action rewards.
366 std::optional<std::vector<ValueType>> optionalStateActionRewardVector;
367
368 // An (optional) matrix representing the transition rewards.
369 std::optional<storm::storage::SparseMatrix<ValueType>> optionalTransitionRewardMatrix;
370};
371
372template<typename ValueType>
373std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueType> const& rewardModel);
374
375std::set<storm::RationalFunctionVariable> getRewardModelParameters(StandardRewardModel<storm::RationalFunction> const& rewModel);
376} // namespace sparse
377} // namespace models
378} // 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 & operator=(StandardRewardModel< ValueType > const &other)=default
friend std::ostream & operator<<(std::ostream &out, StandardRewardModel< ValueTypePrime > const &rewardModel)
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...
StandardRewardModel(StandardRewardModel< ValueType > const &other)=default
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 & operator=(StandardRewardModel< ValueType > &&other)=default
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...
StandardRewardModel(StandardRewardModel< ValueType > &&other)=default
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:16
A class that holds a possibly non-square matrix in the compressed row storage format.
std::set< storm::RationalFunctionVariable > getRewardModelParameters(StandardRewardModel< storm::RationalFunction > const &rewModel)
LabParser.cpp.
constexpr NullRefType NullRef
Definition OptionalRef.h:31