Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
TransitionReward.cpp
Go to the documentation of this file.
3
4namespace storm {
5namespace prism {
6TransitionReward::TransitionReward(uint_fast64_t actionIndex, std::string const& actionName,
7 storm::expressions::Expression const& sourceStatePredicateExpression,
8 storm::expressions::Expression const& targetStatePredicateExpression,
9 storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber)
10 : LocatedInformation(filename, lineNumber),
11 actionIndex(actionIndex),
12 actionName(actionName),
13 labeled(actionName != ""),
14 sourceStatePredicateExpression(sourceStatePredicateExpression),
15 targetStatePredicateExpression(targetStatePredicateExpression),
16 rewardValueExpression(rewardValueExpression) {
17 // Nothing to do here.
18}
19
20std::string const& TransitionReward::getActionName() const {
21 return this->actionName;
22}
23
24uint_fast64_t TransitionReward::getActionIndex() const {
25 return this->actionIndex;
26}
27
29 return this->sourceStatePredicateExpression;
30}
31
33 return this->targetStatePredicateExpression;
34}
35
37 return this->rewardValueExpression;
38}
39
41 return labeled;
42}
43
44TransitionReward TransitionReward::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
46 this->getTargetStatePredicateExpression().substitute(substitution), this->getRewardValueExpression().substitute(substitution),
47 this->getFilename(), this->getLineNumber());
48}
49
50std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward) {
51 stream << "\t[" << transitionReward.getActionName() << "] " << transitionReward.getSourceStatePredicateExpression() << " -> "
52 << transitionReward.getTargetStatePredicateExpression() << ": " << transitionReward.getRewardValueExpression() << ";";
53 return stream;
54}
55
56} // namespace prism
57} // namespace storm
uint_fast64_t getLineNumber() const
Retrieves the line number in which the information was found.
std::string const & getFilename() const
Retrieves the name of the file in which the information was found.
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).
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.
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.
std::string const & getActionName() const
Retrieves the action name that is associated with this transition reward.
std::ostream & operator<<(std::ostream &stream, Assignment const &assignment)
LabParser.cpp.
Definition cli.cpp:18