Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StateActionReward.h
Go to the documentation of this file.
1#ifndef STORM_STORAGE_PRISM_STATEACTIONREWARD_H_
2#define STORM_STORAGE_PRISM_STATEACTIONREWARD_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:
34 StateActionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression,
35 storm::expressions::Expression const& rewardValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
36
37 // Create default implementations of constructors/assignment.
38 StateActionReward() = default;
39 StateActionReward(StateActionReward const& other) = default;
43
49 std::string const& getActionName() const;
50
56 uint_fast64_t getActionIndex() const;
57
64
71
77 bool isLabeled() const;
78
85 StateActionReward substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
86
87 friend std::ostream& operator<<(std::ostream& stream, StateActionReward const& stateActionReward);
88
89 private:
90 // The index of the action name.
91 uint_fast64_t actionIndex;
92
93 // The name of the command this transition-based reward is attached to.
94 std::string actionName;
95
96 // A flag that stores whether the transition reward has an action label.
97 bool labeled;
98
99 // A predicate that needs to be satisfied by states for the reward to be obtained (by taking
100 // a corresponding command transition).
101 storm::expressions::Expression statePredicateExpression;
102
103 // The expression specifying the value of the reward obtained along the transitions.
104 storm::expressions::Expression rewardValueExpression;
105};
106
107} // namespace prism
108} // namespace storm
109
110#endif /* STORM_STORAGE_PRISM_STATEACTIONREWARD_H_ */
StateActionReward(StateActionReward const &other)=default
StateActionReward & operator=(StateActionReward &&other)=default
StateActionReward(StateActionReward &&other)=default
std::string const & getActionName() const
Retrieves the action name that is associated with this transition reward.
storm::expressions::Expression const & getRewardValueExpression() const
Retrieves the reward value expression associated with this state reward.
friend std::ostream & operator<<(std::ostream &stream, StateActionReward const &stateActionReward)
storm::expressions::Expression const & getStatePredicateExpression() const
Retrieves the state predicate expression that is associated with this state reward.
bool isLabeled() const
Retrieves whether the transition reward has an action label.
uint_fast64_t getActionIndex() const
Retrieves the action index of the action associated with this transition reward (if any).
StateActionReward & operator=(StateActionReward const &other)=default
StateActionReward substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all identifiers in the transition reward according to the given map.
LabParser.cpp.
Definition cli.cpp:18