Storm
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
12
13namespace storm {
14namespace models {
15namespace sparse {
16template<typename CValueType>
18 public:
19 typedef CValueType ValueType;
20
28 StandardRewardModel(std::optional<std::vector<ValueType>> const& optionalStateRewardVector = std::nullopt,
29 std::optional<std::vector<ValueType>> const& optionalStateActionRewardVector = std::nullopt,
30 std::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix = std::nullopt);
31
39 StandardRewardModel(std::optional<std::vector<ValueType>>&& optionalStateRewardVector,
40 std::optional<std::vector<ValueType>>&& optionalStateActionRewardVector = std::nullopt,
41 std::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix = std::nullopt);
42
45
48
54 bool hasStateRewards() const;
55
61 bool hasOnlyStateRewards() const;
62
69 std::vector<ValueType> const& getStateRewardVector() const;
70
77 std::vector<ValueType>& getStateRewardVector();
78
79 ValueType const& getStateReward(uint_fast64_t state) const;
80
81 template<typename T>
82 void setStateReward(uint_fast64_t state, T const& newReward);
83
84 // template<typename T=ValueType, EnableIf<hasTotalOrder<T>>>
85 // ValueType maximalStateReward(uint_fast64_t state) const;
86
92 std::optional<std::vector<ValueType>> const& getOptionalStateRewardVector() const;
93
99 bool hasStateActionRewards() const;
100
107 std::vector<ValueType> const& getStateActionRewardVector() const;
108
115 std::vector<ValueType>& getStateActionRewardVector();
116
120 ValueType const& getStateActionReward(uint_fast64_t choiceIndex) const;
121
125 template<typename T>
126 void setStateActionReward(uint_fast64_t choiceIndex, T const& newValue);
127
131 template<typename MatrixValueType>
132 void clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix<MatrixValueType> const& transitions);
133
139 std::optional<std::vector<ValueType>> const& getOptionalStateActionRewardVector() const;
140
146 bool hasTransitionRewards() const;
147
155
163
169 std::optional<storm::storage::SparseMatrix<ValueType>> const& getOptionalTransitionRewardMatrix() const;
170
177 template<typename MatrixValueType>
178 ValueType getStateActionAndTransitionReward(uint_fast64_t choiceIndex, storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const;
179
190 template<typename MatrixValueType>
191 ValueType getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex,
192 storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
193 MatrixValueType const& stateRewardWeight = storm::utility::one<MatrixValueType>(),
194 MatrixValueType const& actionRewardWeight = storm::utility::one<MatrixValueType>()) const;
195
203
209 StandardRewardModel<ValueType> permuteActions(std::vector<uint64_t> const& inversePermutation) const;
210
218 StandardRewardModel<ValueType> permuteStates(std::vector<uint64_t> const& inversePermutation,
219 storm::OptionalRef<std::vector<uint64_t> const> rowGroupIndices = storm::NullRef,
220 storm::OptionalRef<std::vector<uint64_t> const> permutation = storm::NullRef) const;
221
234 template<typename MatrixValueType>
235 void reduceToStateBasedRewards(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, bool reduceToStateRewards = false,
236 std::vector<MatrixValueType> const* weights = nullptr);
237
245 template<typename MatrixValueType>
246 std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const;
247
256 template<typename MatrixValueType>
257 std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
258 std::vector<MatrixValueType> const& weights) const;
259
269 template<typename MatrixValueType>
270 std::vector<ValueType> getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
271 storm::storage::BitVector const& filter) const;
272
282 template<typename MatrixValueType>
283 std::vector<ValueType> getTotalActionRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
284 std::vector<MatrixValueType> const& stateRewardWeights) const;
285
292 template<typename MatrixValueType>
294
299 template<typename MatrixValueType>
301 std::function<bool(ValueType const&)> const& filter) const;
302
309 template<typename MatrixValueType>
311
316 template<typename MatrixValueType>
318 std::function<bool(ValueType const&)> const& filter) const;
319
326 bool empty() const;
327
333 bool isAllZero() const;
334
345 bool isCompatible(uint_fast64_t nrStates, uint_fast64_t nrChoices) const;
346
347 std::size_t hash() const;
348
349 template<typename ValueTypePrime>
350 friend std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueTypePrime> const& rewardModel);
351
352 private:
353 // An (optional) vector representing the state rewards.
354 std::optional<std::vector<ValueType>> optionalStateRewardVector;
355
356 // An (optional) vector representing the state-action rewards.
357 std::optional<std::vector<ValueType>> optionalStateActionRewardVector;
358
359 // An (optional) matrix representing the transition rewards.
360 std::optional<storm::storage::SparseMatrix<ValueType>> optionalTransitionRewardMatrix;
361};
362
363template<typename ValueType>
364std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueType> const& rewardModel);
365
366std::set<storm::RationalFunctionVariable> getRewardModelParameters(StandardRewardModel<storm::RationalFunction> const& rewModel);
367} // namespace sparse
368} // namespace models
369} // 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:18
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)
std::ostream & operator<<(std::ostream &out, ChoiceLabeling const &labeling)
LabParser.cpp.
Definition cli.cpp:18
constexpr NullRefType NullRef
Definition OptionalRef.h:31