Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
TransitionReward.h
Go to the documentation of this file.
1#ifndef STORM_STORAGE_PRISM_TRANSITIONREWARD_H_
2#define STORM_STORAGE_PRISM_TRANSITIONREWARD_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:
36 TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& sourceStatePredicateExpression,
37 storm::expressions::Expression const& targetStatePredicateExpression, storm::expressions::Expression const& rewardValueExpression,
38 std::string const& filename = "", uint_fast64_t lineNumber = 0);
39
40 // Create default implementations of constructors/assignment.
41 TransitionReward() = default;
42 TransitionReward(TransitionReward const& other) = default;
46
52 std::string const& getActionName() const;
53
59 uint_fast64_t getActionIndex() const;
60
67
74
81
87 bool isLabeled() const;
88
95 TransitionReward substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
96
97 friend std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward);
98
99 private:
100 // The index of the action name.
101 uint_fast64_t actionIndex;
102
103 // The name of the command this transition-based reward is attached to.
104 std::string actionName;
105
106 // A flag that stores whether the transition reward has an action label.
107 bool labeled;
108
109 // A predicate that needs to be satisfied in the source state of transitions that can earn the reward.
110 storm::expressions::Expression sourceStatePredicateExpression;
111
112 // A predicate that needs to be satisfied in the target state of transitions that can earn the reward.
113 storm::expressions::Expression targetStatePredicateExpression;
114
115 // The expression specifying the value of the reward obtained along the transitions.
116 storm::expressions::Expression rewardValueExpression;
117};
118
119} // namespace prism
120} // namespace storm
121
122#endif /* STORM_STORAGE_PRISM_TRANSITIONREWARD_H_ */
TransitionReward substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all identifiers in the transition reward according to the given map.
uint_fast64_t getActionIndex() const
Retrieves the action index of the action associated with this transition reward (if any).
TransitionReward(TransitionReward &&other)=default
storm::expressions::Expression const & getRewardValueExpression() const
Retrieves the reward value expression associated with this state reward.
storm::expressions::Expression const & getSourceStatePredicateExpression() const
Retrieves the source state predicate expression that is associated with this state reward.
TransitionReward & operator=(TransitionReward const &other)=default
friend std::ostream & operator<<(std::ostream &stream, TransitionReward const &transitionReward)
TransitionReward & operator=(TransitionReward &&other)=default
bool isLabeled() const
Retrieves whether the transition reward has an action label.
storm::expressions::Expression const & getTargetStatePredicateExpression() const
Retrieves the target state predicate expression that is associated with this state reward.
TransitionReward(TransitionReward const &other)=default
std::string const & getActionName() const
Retrieves the action name that is associated with this transition reward.
LabParser.cpp.
Definition cli.cpp:18