Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
RewardModel.cpp
Go to the documentation of this file.
2
3namespace storm {
4namespace prism {
5RewardModel::RewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards,
6 std::vector<storm::prism::StateActionReward> const& stateActionRewards,
7 std::vector<storm::prism::TransitionReward> const& transitionRewards, std::string const& filename, uint_fast64_t lineNumber)
8 : LocatedInformation(filename, lineNumber),
9 rewardModelName(rewardModelName),
10 stateRewards(stateRewards),
11 stateActionRewards(stateActionRewards),
12 transitionRewards(transitionRewards) {
13 // Nothing to do here.
14}
15
16std::string const& RewardModel::getName() const {
17 return this->rewardModelName;
18}
19
20bool RewardModel::empty() const {
21 return !this->hasStateRewards() && !this->hasTransitionRewards();
22}
23
25 return !this->stateRewards.empty();
26}
27
28std::vector<storm::prism::StateReward> const& RewardModel::getStateRewards() const {
29 return this->stateRewards;
30}
31
33 return !this->stateActionRewards.empty();
34}
35
36std::vector<storm::prism::StateActionReward> const& RewardModel::getStateActionRewards() const {
37 return this->stateActionRewards;
38}
39
41 return !this->transitionRewards.empty();
42}
43
44std::vector<storm::prism::TransitionReward> const& RewardModel::getTransitionRewards() const {
45 return this->transitionRewards;
46}
47
48RewardModel RewardModel::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
49 std::vector<StateReward> newStateRewards;
50 newStateRewards.reserve(this->getStateRewards().size());
51 for (auto const& stateReward : this->getStateRewards()) {
52 newStateRewards.emplace_back(stateReward.substitute(substitution));
53 }
54
55 std::vector<StateActionReward> newStateActionRewards;
56 newStateActionRewards.reserve(this->getStateRewards().size());
57 for (auto const& stateActionReward : this->getStateActionRewards()) {
58 newStateActionRewards.emplace_back(stateActionReward.substitute(substitution));
59 }
60
61 std::vector<TransitionReward> newTransitionRewards;
62 newTransitionRewards.reserve(this->getTransitionRewards().size());
63 for (auto const& transitionReward : this->getTransitionRewards()) {
64 newTransitionRewards.emplace_back(transitionReward.substitute(substitution));
65 }
66 return RewardModel(this->getName(), newStateRewards, newStateActionRewards, newTransitionRewards, this->getFilename(), this->getLineNumber());
67}
68
69bool RewardModel::containsVariablesOnlyInRewardValueExpressions(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
70 for (auto const& stateReward : this->getStateRewards()) {
71 if (stateReward.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
72 return false;
73 }
74 }
75 for (auto const& stateActionReward : this->getStateActionRewards()) {
76 if (stateActionReward.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
77 return false;
78 }
79 }
80 for (auto const& transitionReward : this->getTransitionRewards()) {
81 if (transitionReward.getSourceStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
82 return false;
83 }
84 if (transitionReward.getTargetStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
85 return false;
86 }
87 }
88 return true;
89}
90
92 std::vector<StateActionReward> newStateActionRewards;
93 for (auto const& stateActionReward : this->getStateActionRewards()) {
94 if (actionIndicesToKeep.find(stateActionReward.getActionIndex()) != actionIndicesToKeep.end()) {
95 newStateActionRewards.emplace_back(stateActionReward);
96 }
97 }
98
99 std::vector<TransitionReward> newTransitionRewards;
100 for (auto const& transitionReward : this->getTransitionRewards()) {
101 if (actionIndicesToKeep.find(transitionReward.getActionIndex()) != actionIndicesToKeep.end()) {
102 newTransitionRewards.emplace_back(transitionReward);
103 }
104 }
105
106 return RewardModel(this->getName(), this->getStateRewards(), newStateActionRewards, newTransitionRewards, this->getFilename(), this->getLineNumber());
107}
108
109RewardModel RewardModel::labelUnlabelledCommands(std::vector<std::pair<uint64_t, std::string>> const& newActions) const {
110 std::vector<StateActionReward> newStateActionRewards;
111 std::vector<TransitionReward> newTransitionRewards;
112
113 for (auto const& reward : getStateActionRewards()) {
114 if (reward.getActionIndex() == 0) {
115 for (auto const& newAction : newActions) {
116 newStateActionRewards.emplace_back(newAction.first, newAction.second, reward.getStatePredicateExpression(), reward.getRewardValueExpression(),
117 reward.getFilename(), reward.getLineNumber());
118 }
119 } else {
120 newStateActionRewards.push_back(reward);
121 }
122 }
123
124 assert(transitionRewards.empty()); // Not implemented.
125
126 return RewardModel(this->getName(), this->getStateRewards(), newStateActionRewards, newTransitionRewards, this->getFilename(), this->getLineNumber());
127}
128
129std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) {
130 stream << "rewards";
131 if (rewardModel.getName() != "") {
132 stream << " \"" << rewardModel.getName() << "\"";
133 }
134 stream << '\n';
135 for (auto const& reward : rewardModel.getStateRewards()) {
136 stream << reward << '\n';
137 }
138 for (auto const& reward : rewardModel.getStateActionRewards()) {
139 stream << reward << '\n';
140 }
141 for (auto const& reward : rewardModel.getTransitionRewards()) {
142 stream << reward << '\n';
143 }
144 stream << "endrewards\n";
145 return stream;
146}
147
148} // namespace prism
149} // 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.
std::vector< storm::prism::StateReward > const & getStateRewards() const
Retrieves all state rewards associated with this reward model.
bool hasStateRewards() const
Retrieves whether there are any state rewards.
RewardModel labelUnlabelledCommands(std::vector< std::pair< uint64_t, std::string > > const &newActionNames) const
RewardModel substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all variables in the reward model according to the given map.
bool containsVariablesOnlyInRewardValueExpressions(std::set< storm::expressions::Variable > const &undefinedConstantVariables) const
Checks whether any of the given variables only appear in the expressions defining the reward value.
bool hasTransitionRewards() const
Retrieves whether there are any transition rewards.
RewardModel restrictActionRelatedRewards(storm::storage::FlatSet< uint_fast64_t > const &actionIndicesToKeep) const
Restricts all action-related rewards of the reward model to the ones with an action index in the prov...
std::vector< storm::prism::TransitionReward > const & getTransitionRewards() const
Retrieves all transition rewards associated with this reward model.
std::string const & getName() const
Retrieves the name of the reward model.
bool empty() const
Checks whether the reward model is empty, i.e.
bool hasStateActionRewards() const
Retrieves whether there are any state-action rewards.
std::vector< storm::prism::StateActionReward > const & getStateActionRewards() const
Retrieves all state-action rewards associated with this reward model.
std::ostream & operator<<(std::ostream &stream, Assignment const &assignment)
boost::container::flat_set< Key, std::less< Key >, boost::container::new_allocator< Key > > FlatSet
Redefinition of flat_set was needed, because from Boost 1.70 on the default allocator is set to void.
Definition BoostTypes.h:13
LabParser.cpp.
Definition cli.cpp:18