Storm
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 this->distribution[state] += probability;
61}
62
63template<typename ValueType, typename StateType>
64void Distribution<ValueType, StateType>::removeProbability(StateType const& state, ValueType const& probability,
66 auto it = this->distribution.find(state);
67 STORM_LOG_ASSERT(it != this->distribution.end(), "Cannot remove probability, because the state is not in the support of the distribution.");
68 it->second -= probability;
69 if (comparator.isZero(it->second)) {
70 this->distribution.erase(it);
71 }
72}
73
74template<typename ValueType, typename StateType>
75void Distribution<ValueType, StateType>::shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability,
77 removeProbability(fromState, probability, comparator);
78 addProbability(toState, probability);
80
81template<typename ValueType, typename StateType>
85
86template<typename ValueType, typename StateType>
88 return this->distribution.begin();
89}
90
91template<typename ValueType, typename StateType>
95
96template<typename ValueType, typename StateType>
100
101template<typename ValueType, typename StateType>
103 return this->distribution.end();
104}
105
106template<typename ValueType, typename StateType>
108 return this->end();
109}
110
111template<typename ValueType, typename StateType>
112void Distribution<ValueType, StateType>::scale(StateType const& state) {
113 auto probabilityIterator = this->distribution.find(state);
114 if (probabilityIterator != this->distribution.end()) {
115 ValueType scaleValue = storm::utility::one<ValueType>() / probabilityIterator->second;
116 this->distribution.erase(probabilityIterator);
117
118 for (auto& entry : this->distribution) {
119 entry.second *= scaleValue;
120 }
121 }
123
124template<typename ValueType, typename StateType>
126 return this->distribution.size();
127}
128
129template<typename ValueType, typename StateType>
130std::ostream& operator<<(std::ostream& out, Distribution<ValueType, StateType> const& distribution) {
131 out << "{";
132 for (auto const& entry : distribution) {
133 out << "[" << entry.second << ": " << entry.first << "], ";
134 }
135 out << "}";
137 return out;
139
140template<typename ValueType, typename StateType>
142 storm::utility::ConstantsComparator<ValueType> const& comparator) const {
143 if (this->size() != other.size()) {
144 return this->size() < other.size();
146 auto firstIt = this->begin();
147 auto firstIte = this->end();
148 auto secondIt = other.begin();
149 for (; firstIt != firstIte; ++firstIt, ++secondIt) {
150 // If the two blocks already differ, we can decide which distribution is smaller.
151 if (firstIt->first != secondIt->first) {
152 return firstIt->first < secondIt->first;
153 }
154
155 // If the blocks are the same, but the probability differs, we can also decide which distribution is smaller.
156 if (!comparator.isEqual(firstIt->second, secondIt->second)) {
157 return comparator.isLess(firstIt->second, secondIt->second);
158 }
159 }
160 return false;
162
163template<typename ValueType, typename StateType>
164ValueType Distribution<ValueType, StateType>::getProbability(StateType const& state) const {
165 auto it = this->distribution.find(state);
166 if (it == this->distribution.end()) {
167 return storm::utility::zero<ValueType>();
168 } else {
169 return it->second;
170 }
171}
172
173template<typename ValueType, typename StateType>
175 ValueType sum = storm::utility::zero<ValueType>();
176 for (auto const& entry : distribution) {
177 sum += entry.second;
178 }
179 for (auto& entry : distribution) {
180 entry.second /= sum;
181 }
182}
183
184template<typename ValueType, typename StateType>
185typename std::enable_if<!std::is_same<ValueType, storm::RationalFunction>::value, StateType>::type sample(
186 boost::container::flat_map<StateType, ValueType> const& distr, ValueType const& quantile) {
187 ValueType sum = storm::utility::zero<ValueType>();
188 for (auto const& entry : distr) {
189 sum += entry.second;
190 if (quantile < sum) {
191 return entry.first;
192 }
193 }
194 STORM_LOG_ASSERT(false, "This point should not be reached.");
195 return 0;
196}
197
198template<typename ValueType, typename StateType>
199typename std::enable_if<std::is_same<ValueType, storm::RationalFunction>::value, StateType>::type sample(
200 boost::container::flat_map<StateType, storm::RationalFunction> const& distr, storm::RationalFunction const& quantile) {
201 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "We cannot sample from parametric distributions.");
202}
203
204template<typename ValueType, typename StateType>
205StateType Distribution<ValueType, StateType>::sampleFromDistribution(const ValueType& quantile) const {
206 return sample<ValueType, StateType>(this->distribution, quantile);
207}
208
209template class Distribution<double>;
210template std::ostream& operator<<(std::ostream& out, Distribution<double> const& distribution);
211template class Distribution<double, uint64_t>;
212template std::ostream& operator<<(std::ostream& out, Distribution<double, uint_fast64_t> const& distribution);
213
214#ifdef STORM_HAVE_CARL
216template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalNumber> const& distribution);
218template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalNumber, uint_fast64_t> const& distribution);
219
221template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalFunction> const& distribution);
223template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalFunction, uint64_t> const& distribution);
224
225template class Distribution<storm::Interval>;
226template std::ostream& operator<<(std::ostream& out, Distribution<storm::Interval> const& distribution);
228template std::ostream& operator<<(std::ostream& out, Distribution<storm::Interval, uint64_t> const& distribution);
229
230#endif
231} // namespace storage
232} // 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)
std::ostream & operator<<(std::ostream &out, ParameterRegion< ParametricType > const &region)
LabParser.cpp.
Definition cli.cpp:18