Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Choice.cpp
Go to the documentation of this file.
2
11
12namespace storm {
13namespace generator {
14
15template<typename ValueType, typename StateType>
16Choice<ValueType, StateType>::Choice(uint_fast64_t actionIndex, bool markovian)
17 : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero<ValueType>()), rewards(), labels() {
18 // Intentionally left empty.
19}
20
21template<typename ValueType, typename StateType>
22void Choice<ValueType, StateType>::reset(uint_fast64_t newActionIndex, bool newMarkovian) {
23 markovian = newMarkovian;
24 actionIndex = newActionIndex;
25 distribution.clear();
27 rewards.clear();
28 originData = boost::none;
29 labels = boost::none;
30 playerIndex = boost::none;
31}
32
33template<typename ValueType, typename StateType>
35 STORM_LOG_THROW(this->markovian == other.markovian, storm::exceptions::InvalidOperationException, "Type of choices do not match.");
36 STORM_LOG_THROW(this->actionIndex == other.actionIndex, storm::exceptions::InvalidOperationException, "Action index of choices do not match.");
37 STORM_LOG_THROW(this->rewards.size() == other.rewards.size(), storm::exceptions::InvalidOperationException, "Reward value sizes of choices do not match.");
38
39 // Add the elements to the distribution.
40 this->distribution.add(other.distribution);
41
42 // Update the total mass of the choice.
43 this->totalMass += other.totalMass;
44
45 // Add all reward values.
46 auto otherRewIt = other.rewards.begin();
47 for (auto& rewardValue : this->rewards) {
48 rewardValue += *otherRewIt;
49 ++otherRewIt;
50 }
51
52 // Join label sets and origin data if given.
53 if (other.labels) {
54 this->addLabels(other.labels.get());
55 }
56 if (other.originData) {
57 this->addOriginData(other.originData.get());
58 }
59}
60
61template<typename ValueType, typename StateType>
62StateType Choice<ValueType, StateType>::sampleFromDistribution(ValueType const& quantile) const {
63 return distribution.sampleFromDistribution(quantile);
64}
65
66template<typename ValueType, typename StateType>
70
71template<typename ValueType, typename StateType>
75
76template<typename ValueType, typename StateType>
80
81template<typename ValueType, typename StateType>
85
86template<typename ValueType, typename StateType>
87void Choice<ValueType, StateType>::addLabel(std::string const& newLabel) {
88 if (!labels) {
89 labels = std::set<std::string>();
90 }
91 labels->insert(newLabel);
92}
93
94template<typename ValueType, typename StateType>
95void Choice<ValueType, StateType>::addLabels(std::set<std::string> const& newLabels) {
96 if (labels) {
97 labels->insert(newLabels.begin(), newLabels.end());
98 } else {
99 labels = newLabels;
100 }
101}
102
103template<typename ValueType, typename StateType>
105 return labels.is_initialized();
106}
107
108template<typename ValueType, typename StateType>
109std::set<std::string> const& Choice<ValueType, StateType>::getLabels() const {
110 return labels.get();
111}
112
113template<typename ValueType, typename StateType>
115 this->playerIndex = playerIndex;
116}
117
118template<typename ValueType, typename StateType>
120 return playerIndex.is_initialized();
121}
122
123template<typename ValueType, typename StateType>
125 return playerIndex.get();
126}
127
128template<typename ValueType, typename StateType>
130 if (!this->originData || this->originData->empty()) {
131 this->originData = data;
132 } else {
133 if (!data.empty()) {
134 // Reaching this point means that the both the existing and the given data are non-empty
135
136 auto existingDataAsIndexSet = boost::any_cast<storm::storage::FlatSet<uint_fast64_t>>(&this->originData.get());
137 if (existingDataAsIndexSet != nullptr) {
138 auto givenDataAsIndexSet = boost::any_cast<storm::storage::FlatSet<uint_fast64_t>>(&data);
139 STORM_LOG_THROW(givenDataAsIndexSet != nullptr, storm::exceptions::InvalidOperationException,
140 "Types of existing and given choice origin data do not match.");
141 existingDataAsIndexSet->insert(givenDataAsIndexSet->begin(), givenDataAsIndexSet->end());
142 } else {
143 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
144 "Type of choice origin data (aka " << data.type().name() << ") is not implemented.");
145 }
146 }
147 }
148}
149
150template<typename ValueType, typename StateType>
152 return originData.is_initialized();
153}
154
155template<typename ValueType, typename StateType>
157 return originData.get();
158}
159
160template<typename ValueType, typename StateType>
162 return actionIndex;
163}
164
165template<typename ValueType, typename StateType>
167 return totalMass;
168}
169
170template<typename ValueType, typename StateType>
171void Choice<ValueType, StateType>::addProbability(StateType const& state, ValueType const& value) {
172 totalMass += value;
173 distribution.addProbability(state, value);
174}
175
176template<typename ValueType, typename StateType>
177void Choice<ValueType, StateType>::addReward(ValueType const& value) {
178 rewards.push_back(value);
179}
180
181template<typename ValueType, typename StateType>
182void Choice<ValueType, StateType>::addRewards(std::vector<ValueType>&& values) {
183 this->rewards = std::move(values);
184}
185
186template<typename ValueType, typename StateType>
187std::vector<ValueType> const& Choice<ValueType, StateType>::getRewards() const {
188 return rewards;
189}
190
191template<typename ValueType, typename StateType>
193 return rewards;
194}
195
196template<typename ValueType, typename StateType>
198 return markovian;
199}
200
201template<typename ValueType, typename StateType>
203 return distribution.size();
204}
205
206template<typename ValueType, typename StateType>
208 distribution.reserve(size);
209}
210
211template<typename ValueType, typename StateType>
212std::ostream& operator<<(std::ostream& out, Choice<ValueType, StateType> const& choice) {
213 out << "<";
214 for (auto const& stateProbabilityPair : choice) {
215 out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", ";
216 }
217 out << ">";
218 return out;
219}
220
221template struct Choice<double>;
222
223template struct Choice<storm::RationalNumber>;
224template struct Choice<storm::RationalFunction>;
225template struct Choice<storm::Interval>;
226template struct Choice<storm::RationalInterval>;
227} // namespace generator
228} // namespace storm
container_type::const_iterator const_iterator
container_type::iterator iterator
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:39
std::ostream & operator<<(std::ostream &out, Choice< ValueType, StateType > const &choice)
Definition Choice.cpp:212
uint64_t PlayerIndex
Definition PlayerIndex.h:7
ValueType zero()
Definition constants.cpp:26
bool hasLabels() const
Returns whether there are labels defined for this choice.
Definition Choice.cpp:104
bool isMarkovian() const
Retrieves whether the choice is Markovian.
Definition Choice.cpp:197
boost::any const & getOriginData() const
Returns the origin data associated with this choice.
Definition Choice.cpp:156
void addLabel(std::string const &label)
Adds the given label to the labels associated with this choice.
Definition Choice.cpp:87
uint_fast64_t getActionIndex() const
Retrieves the index of the action of this choice.
Definition Choice.cpp:161
storm::storage::Distribution< ValueType, StateType >::iterator end()
Returns an iterator past the end of the distribution associated with this choice.
Definition Choice.cpp:77
std::vector< ValueType > const & getRewards() const
Retrieves the rewards for this choice under selected reward models.
Definition Choice.cpp:187
std::set< std::string > const & getLabels() const
Retrieves the set of labels associated with this choice.
Definition Choice.cpp:109
void add(Choice const &other)
Adds the given choice to the current one.
Definition Choice.cpp:34
ValueType getTotalMass() const
Retrieves the total mass of this choice.
Definition Choice.cpp:166
void addOriginData(boost::any const &data)
Adds the given data that specifies the origin of this choice w.r.t.
Definition Choice.cpp:129
void setPlayerIndex(storm::storage::PlayerIndex const &playerIndex)
Sets the players index.
Definition Choice.cpp:114
storm::storage::PlayerIndex const & getPlayerIndex() const
Retrieves the players index associated with this choice.
Definition Choice.cpp:124
Choice(uint_fast64_t actionIndex=0, bool markovian=false)
Definition Choice.cpp:16
void addLabels(std::set< std::string > const &labels)
Adds the given label set to the labels associated with this choice.
Definition Choice.cpp:95
bool hasOriginData() const
Returns whether there is origin data defined for this choice.
Definition Choice.cpp:151
void addRewards(std::vector< ValueType > &&values)
Adds the given choices rewards to this choice.
Definition Choice.cpp:182
StateType sampleFromDistribution(ValueType const &quantile) const
Given a value q, find the event in the ordered distribution that corresponds to this prob.
Definition Choice.cpp:62
storm::storage::Distribution< ValueType, StateType >::iterator begin()
Returns an iterator to the distribution associated with this choice.
Definition Choice.cpp:67
void reset(uint_fast64_t actionIndex=0, bool markovian=false)
Resets this choice to an empty choice with the given action index (i.e., as if it was newly construct...
Definition Choice.cpp:22
void reserve(std::size_t const &size)
If the size is already known, reserves space in the underlying distribution.
Definition Choice.cpp:207
bool hasPlayerIndex() const
Returns whether there is an index for the player defined for this choice.
Definition Choice.cpp:119
std::size_t size() const
Retrieves the size of the distribution associated with this choice.
Definition Choice.cpp:202
void addProbability(StateType const &state, ValueType const &value)
Adds the given probability value to the given state in the underlying distribution.
Definition Choice.cpp:171
void addReward(ValueType const &value)
Adds the given value to the reward associated with this choice.
Definition Choice.cpp:177