Storm 1.10.0.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
9
12
13namespace storm {
14namespace storage {
15
16template<typename ValueType, typename StateType>
18 // Intentionally left empty.
19}
20
21template<typename ValueType, typename StateType>
23 this->distribution.reserve(size);
24}
26template<typename ValueType, typename StateType>
28 container_type newDistribution;
29 std::set_union(this->distribution.begin(), this->distribution.end(), other.distribution.begin(), other.distribution.end(),
30 std::inserter(newDistribution, newDistribution.begin()));
31 this->distribution = std::move(newDistribution);
32}
33
34template<typename ValueType, typename StateType>
36 storm::utility::ConstantsComparator<ValueType> const& comparator) const {
37 // We need to check equality by ourselves, because we need to account for epsilon differences.
38 if (this->distribution.size() != other.distribution.size()) {
39 return false;
40 }
41
42 auto first1 = this->distribution.begin();
43 auto last1 = this->distribution.end();
44 auto first2 = other.distribution.begin();
45
46 for (; first1 != last1; ++first1, ++first2) {
47 if (first1->first != first2->first) {
48 return false;
49 }
50 if (!comparator.isEqual(first1->second, first2->second)) {
51 return false;
52 }
53 }
54
55 return true;
56}
58template<typename ValueType, typename StateType>
59void Distribution<ValueType, StateType>::addProbability(StateType const& state, ValueType const& probability) {
60 auto [iterator, newEntry] = this->distribution.try_emplace(state, probability);
61 if (!newEntry) {
62 iterator->second += probability;
63 }
64}
65
66template<typename ValueType, typename StateType>
67void Distribution<ValueType, StateType>::removeProbability(StateType const& state, ValueType const& probability,
69 auto it = this->distribution.find(state);
70 STORM_LOG_ASSERT(it != this->distribution.end(), "Cannot remove probability, because the state is not in the support of the distribution.");
71 it->second -= probability;
72 if (comparator.isZero(it->second)) {
73 this->distribution.erase(it);
74 }
75}
76
77template<typename ValueType, typename StateType>
78void Distribution<ValueType, StateType>::shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability,
80 removeProbability(fromState, probability, comparator);
81 addProbability(toState, probability);
82}
83
84template<typename ValueType, typename StateType>
88
89template<typename ValueType, typename StateType>
91 return this->distribution.begin();
92}
93
94template<typename ValueType, typename StateType>
98
99template<typename ValueType, typename StateType>
101 return this->distribution.end();
102}
103
104template<typename ValueType, typename StateType>
106 return this->distribution.end();
107}
109template<typename ValueType, typename StateType>
113
114template<typename ValueType, typename StateType>
115void Distribution<ValueType, StateType>::scale(StateType const& state) {
116 auto probabilityIterator = this->distribution.find(state);
117 if (probabilityIterator != this->distribution.end()) {
118 ValueType scaleValue = storm::utility::one<ValueType>() / probabilityIterator->second;
119 this->distribution.erase(probabilityIterator);
120
121 for (auto& entry : this->distribution) {
122 entry.second *= scaleValue;
123 }
124 }
125}
126
127template<typename ValueType, typename StateType>
129 return this->distribution.size();
130}
132template<typename ValueType, typename StateType>
133std::ostream& operator<<(std::ostream& out, Distribution<ValueType, StateType> const& distribution) {
134 out << "{";
135 for (auto const& entry : distribution) {
136 out << "[" << entry.second << ": " << entry.first << "], ";
137 }
138 out << "}";
139
140 return out;
141}
142
143template<typename ValueType, typename StateType>
146 if (this->size() != other.size()) {
147 return this->size() < other.size();
148 }
149 auto firstIt = this->begin();
150 auto firstIte = this->end();
151 auto secondIt = other.begin();
152 for (; firstIt != firstIte; ++firstIt, ++secondIt) {
153 // If the two blocks already differ, we can decide which distribution is smaller.
154 if (firstIt->first != secondIt->first) {
155 return firstIt->first < secondIt->first;
156 }
157
158 // If the blocks are the same, but the probability differs, we can also decide which distribution is smaller.
159 if (!comparator.isEqual(firstIt->second, secondIt->second)) {
160 return comparator.isLess(firstIt->second, secondIt->second);
162 }
163 return false;
164}
165
166template<typename ValueType, typename StateType>
167ValueType Distribution<ValueType, StateType>::getProbability(StateType const& state) const {
168 auto it = this->distribution.find(state);
169 if (it == this->distribution.end()) {
170 return storm::utility::zero<ValueType>();
171 } else {
172 return it->second;
173 }
174}
175
176template<typename ValueType, typename StateType>
178 ValueType sum = storm::utility::zero<ValueType>();
179 for (auto const& entry : distribution) {
180 sum += entry.second;
181 }
182 for (auto& entry : distribution) {
183 entry.second /= sum;
184 }
185}
186
187template<typename ValueType, typename StateType>
188typename std::enable_if<!std::is_same<ValueType, storm::RationalFunction>::value, StateType>::type sample(
189 boost::container::flat_map<StateType, ValueType> const& distr, ValueType const& quantile) {
190 ValueType sum = storm::utility::zero<ValueType>();
191 for (auto const& entry : distr) {
192 sum += entry.second;
193 if (quantile < sum) {
194 return entry.first;
195 }
196 }
197 STORM_LOG_ASSERT(false, "This point should not be reached.");
198 return 0;
199}
200
201template<typename ValueType, typename StateType>
202typename std::enable_if<std::is_same<ValueType, storm::RationalFunction>::value, StateType>::type sample(
203 boost::container::flat_map<StateType, storm::RationalFunction> const& distr, storm::RationalFunction const& quantile) {
204 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "We cannot sample from parametric distributions.");
205}
206
207template<typename ValueType, typename StateType>
208StateType Distribution<ValueType, StateType>::sampleFromDistribution(const ValueType& quantile) const {
209 return sample<ValueType, StateType>(this->distribution, quantile);
210}
211
212template class Distribution<double>;
213template std::ostream& operator<<(std::ostream& out, Distribution<double> const& distribution);
214template class Distribution<double, uint64_t>;
215template std::ostream& operator<<(std::ostream& out, Distribution<double, uint_fast64_t> const& distribution);
216
217#ifdef STORM_HAVE_CARL
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#endif
234} // namespace storage
235} // namespace storm
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
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 shiftProbability(StateType const &fromState, StateType const &toState, ValueType const &probability, storm::utility::ConstantsComparator< ValueType > const &comparator=storm::utility::ConstantsComparator< ValueType >())
Removes the probability mass from one state and adds it to another.
void normalize()
Normalizes the distribution such that the values sum up to one.
bool equals(Distribution< ValueType, StateType > const &other, storm::utility::ConstantsComparator< ValueType > const &comparator=storm::utility::ConstantsComparator< ValueType >()) const
Checks whether the two distributions specify the same probabilities to go to the same states.
container_type::const_iterator const_iterator
const_iterator cbegin() const
Retrieves an iterator to the elements in this distribution.
void removeProbability(StateType const &state, ValueType const &probability, storm::utility::ConstantsComparator< ValueType > const &comparator=storm::utility::ConstantsComparator< ValueType >())
Removes the given probability mass of going to the given state.
std::size_t size() const
Retrieves the size of the distribution, i.e.
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 isZero(ValueType const &value) const
bool isEqual(ValueType const &value1, ValueType const &value2) const
bool isLess(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)
LabParser.cpp.