Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Distribution.cpp
Go to the documentation of this file.
2
3#include <algorithm>
4#include <iostream>
5
13
14namespace storm {
15namespace storage {
16
17template<typename ValueType, typename StateType>
19 // Intentionally left empty.
20}
21
22template<typename ValueType, typename StateType>
24 this->distribution.reserve(size);
26
27template<typename ValueType, typename StateType>
29 container_type newDistribution;
30 std::set_union(this->distribution.begin(), this->distribution.end(), other.distribution.begin(), other.distribution.end(),
31 std::inserter(newDistribution, newDistribution.begin()));
32 this->distribution = std::move(newDistribution);
33}
34
35template<typename ValueType, typename StateType>
37 storm::utility::ConstantsComparator<ValueType> const& comparator) const {
38 // We need to check equality by ourselves, because we need to account for epsilon differences.
39 if (this->distribution.size() != other.distribution.size()) {
40 return false;
41 }
42
43 auto first1 = this->distribution.begin();
44 auto last1 = this->distribution.end();
45 auto first2 = other.distribution.begin();
46
47 for (; first1 != last1; ++first1, ++first2) {
48 if (first1->first != first2->first) {
49 return false;
50 }
51 if (!comparator.isEqual(first1->second, first2->second)) {
52 return false;
53 }
54 }
55
56 return true;
57}
58
59template<typename ValueType, typename StateType>
60void Distribution<ValueType, StateType>::addProbability(StateType const& state, ValueType const& probability) {
61 auto [iterator, newEntry] = this->distribution.try_emplace(state, probability);
62 if (!newEntry) {
63 iterator->second += probability;
64 }
65}
67template<typename ValueType, typename StateType>
68void Distribution<ValueType, StateType>::removeProbability(StateType const& state, ValueType const& probability,
70 auto it = this->distribution.find(state);
71 STORM_LOG_ASSERT(it != this->distribution.end(), "Cannot remove probability, because the state is not in the support of the distribution.");
72 it->second -= probability;
73 if (comparator.isZero(it->second)) {
74 this->distribution.erase(it);
75 }
76}
78template<typename ValueType, typename StateType>
79void Distribution<ValueType, StateType>::shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability,
81 removeProbability(fromState, probability, comparator);
82 addProbability(toState, probability);
83}
84
85template<typename ValueType, typename StateType>
89
90template<typename ValueType, typename StateType>
94
95template<typename ValueType, typename StateType>
100template<typename ValueType, typename StateType>
104
105template<typename ValueType, typename StateType>
107 return this->distribution.end();
108}
109
110template<typename ValueType, typename StateType>
114
115template<typename ValueType, typename StateType>
116void Distribution<ValueType, StateType>::scale(StateType const& state) {
117 auto probabilityIterator = this->distribution.find(state);
118 if (probabilityIterator != this->distribution.end()) {
119 ValueType scaleValue = storm::utility::one<ValueType>() / probabilityIterator->second;
120 this->distribution.erase(probabilityIterator);
121
122 for (auto& entry : this->distribution) {
123 entry.second *= scaleValue;
124 }
125 }
126}
127
128template<typename ValueType, typename StateType>
130 return this->distribution.size();
131}
132
133template<typename ValueType, typename StateType>
134std::ostream& operator<<(std::ostream& out, Distribution<ValueType, StateType> const& distribution) {
135 out << "{";
136 for (auto const& entry : distribution) {
137 out << "[" << entry.second << ": " << entry.first << "], ";
138 }
139 out << "}";
140
141 return out;
142}
144template<typename ValueType, typename StateType>
146 storm::utility::ConstantsComparator<ValueType> const& comparator) const {
147 if (this->size() != other.size()) {
148 return this->size() < other.size();
149 }
150 auto firstIt = this->begin();
151 auto firstIte = this->end();
152 auto secondIt = other.begin();
153 for (; firstIt != firstIte; ++firstIt, ++secondIt) {
154 // If the two blocks already differ, we can decide which distribution is smaller.
155 if (firstIt->first != secondIt->first) {
156 return firstIt->first < secondIt->first;
157 }
158
159 // If the blocks are the same, but the probability differs, we can also decide which distribution is smaller.
160 if (!comparator.isEqual(firstIt->second, secondIt->second)) {
161 return comparator.isLess(firstIt->second, secondIt->second);
162 }
163 }
164 return false;
165}
166
167template<typename ValueType, typename StateType>
168ValueType Distribution<ValueType, StateType>::getProbability(StateType const& state) const {
169 auto it = this->distribution.find(state);
170 if (it == this->distribution.end()) {
171 return storm::utility::zero<ValueType>();
172 } else {
173 return it->second;
174 }
175}
176
177template<typename ValueType, typename StateType>
179 ValueType sum = storm::utility::zero<ValueType>();
180 for (auto const& entry : distribution) {
181 sum += entry.second;
182 }
183 for (auto& entry : distribution) {
184 entry.second /= sum;
185 }
186}
187
188template<typename ValueType, typename StateType>
189typename std::enable_if<!std::is_same<ValueType, storm::RationalFunction>::value, StateType>::type sample(
190 boost::container::flat_map<StateType, ValueType> const& distr, ValueType const& quantile) {
191 ValueType sum = storm::utility::zero<ValueType>();
192 for (auto const& entry : distr) {
193 sum += entry.second;
194 if (quantile < sum) {
195 return entry.first;
196 }
197 }
198 STORM_LOG_ASSERT(false, "This point should not be reached.");
199 return 0;
200}
201
202template<typename ValueType, typename StateType>
203typename std::enable_if<std::is_same<ValueType, storm::RationalFunction>::value, StateType>::type sample(
204 boost::container::flat_map<StateType, storm::RationalFunction> const& distr, storm::RationalFunction const& quantile) {
205 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "We cannot sample from parametric distributions.");
206}
207
208template<typename ValueType, typename StateType>
209StateType Distribution<ValueType, StateType>::sampleFromDistribution(const ValueType& quantile) const {
210 return sample<ValueType, StateType>(this->distribution, quantile);
211}
212
213template class Distribution<double>;
214template std::ostream& operator<<(std::ostream& out, Distribution<double> const& distribution);
215template class Distribution<double, uint64_t>;
216template std::ostream& operator<<(std::ostream& out, Distribution<double, uint_fast64_t> const& distribution);
217
219template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalNumber> const& distribution);
221template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalNumber, uint_fast64_t> const& distribution);
222
224template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalFunction> const& distribution);
226template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalFunction, uint64_t> const& distribution);
227
228template class Distribution<storm::Interval>;
229template std::ostream& operator<<(std::ostream& out, Distribution<storm::Interval> const& distribution);
231template std::ostream& operator<<(std::ostream& out, Distribution<storm::Interval, uint64_t> const& distribution);
232
233} // namespace storage
234} // namespace storm
void shiftProbability(StateType const &fromState, StateType const &toState, ValueType const &probability, storm::utility::ConstantsComparator< ValueType > const &comparator)
Removes the probability mass from one state and adds it to another.
iterator end()
Retrieves an iterator past the elements in this distribution.
void reserve(uint64_t size)
void addProbability(StateType const &state, ValueType const &probability)
Assigns the given state the given probability under this distribution.
boost::container::flat_map< StateType, ValueType > container_type
void removeProbability(StateType const &state, ValueType const &probability, storm::utility::ConstantsComparator< ValueType > const &comparator)
Removes the given probability mass of going to the given state.
const_iterator cend() const
Retrieves an iterator past the elements in this distribution.
bool less(Distribution< ValueType, StateType > const &other, storm::utility::ConstantsComparator< ValueType > const &comparator) const
void normalize()
Normalizes the distribution such that the values sum up to one.
container_type::const_iterator const_iterator
const_iterator cbegin() const
Retrieves an iterator to the elements in this distribution.
std::size_t size() const
Retrieves the size of the distribution, i.e.
bool equals(Distribution< ValueType, StateType > const &other, storm::utility::ConstantsComparator< ValueType > const &comparator) const
Checks whether the two distributions specify the same probabilities to go to the same states.
StateType sampleFromDistribution(ValueType const &quantile) const
Given a value q, find the event in the ordered distribution that corresponds to this prob.
iterator begin()
Retrieves an iterator to the elements in this distribution.
ValueType getProbability(StateType const &state) const
Returns the probability of the given state.
Distribution()
Creates an empty distribution.
container_type::iterator iterator
void add(Distribution const &other)
Adds the given distribution to the current one.
void scale(StateType const &state)
Scales the distribution by multiplying all the probabilities with 1/p where p is the probability of m...
bool isLess(ValueType const &value1, ValueType const &value2) const
bool isZero(ValueType const &value) const
bool isEqual(ValueType const &value1, ValueType const &value2) const
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, StateType >::type sample(boost::container::flat_map< StateType, ValueType > const &distr, ValueType const &quantile)