Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StateReward.h
Go to the documentation of this file.
1#ifndef STORM_STORAGE_PRISM_STATEREWARD_H_
2#define STORM_STORAGE_PRISM_STATEREWARD_H_
3
4#include <map>
5
9
10namespace storm {
11namespace storage {
12namespace expressions {
13class Variable;
14}
15} // namespace storage
16} // namespace storm
17
18namespace storm {
19namespace prism {
21 public:
31 StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression,
32 std::string const& filename = "", uint_fast64_t lineNumber = 0);
33
34 // Create default implementations of constructors/assignment.
35 StateReward() = default;
36 StateReward(StateReward const& other) = default;
37 StateReward& operator=(StateReward const& other) = default;
38 StateReward(StateReward&& other) = default;
39 StateReward& operator=(StateReward&& other) = default;
40
47
54
61 StateReward substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
62
63 friend std::ostream& operator<<(std::ostream& stream, StateReward const& stateReward);
64
65 private:
66 // The predicate that characterizes the states that obtain this reward.
67 storm::expressions::Expression statePredicateExpression;
68
69 // The expression that specifies the value of the reward obtained.
70 storm::expressions::Expression rewardValueExpression;
71};
72
73} // namespace prism
74} // namespace storm
75
76#endif /* STORM_STORAGE_PRISM_STATEREWARD_H_ */
friend std::ostream & operator<<(std::ostream &stream, StateReward const &stateReward)
storm::expressions::Expression const & getStatePredicateExpression() const
Retrieves the state predicate that is associated with this state reward.
storm::expressions::Expression const & getRewardValueExpression() const
Retrieves the reward value associated with this state reward.
StateReward(StateReward const &other)=default
StateReward & operator=(StateReward const &other)=default
StateReward & operator=(StateReward &&other)=default
StateReward substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all identifiers in the state reward according to the given map.
StateReward(StateReward &&other)=default
LabParser.cpp.
Definition cli.cpp:18