Storm
A Modern Probabilistic Model Checker
|
#include <Distribution.h>
Public Types | |
typedef boost::container::flat_map< StateType, ValueType > | container_type |
typedef container_type::iterator | iterator |
typedef container_type::const_iterator | const_iterator |
Public Member Functions | |
Distribution () | |
Creates an empty distribution. | |
Distribution (Distribution const &other)=default | |
Distribution & | operator= (Distribution const &other)=default |
Distribution (Distribution &&other)=default | |
Distribution & | operator= (Distribution &&other)=default |
void | reserve (uint64_t size) |
void | add (Distribution const &other) |
Adds the given distribution to the current 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. | |
void | addProbability (StateType const &state, ValueType const &probability) |
Assigns the given state the given probability under 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. | |
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. | |
iterator | begin () |
Retrieves an iterator to the elements in this distribution. | |
const_iterator | begin () const |
Retrieves an iterator to the elements in this distribution. | |
const_iterator | cbegin () const |
Retrieves an iterator to the elements in this distribution. | |
iterator | end () |
Retrieves an iterator past the elements in this distribution. | |
const_iterator | end () const |
Retrieves an iterator past the elements in this distribution. | |
const_iterator | cend () const |
Retrieves an iterator past the elements in this distribution. | |
void | scale (StateType const &state) |
Scales the distribution by multiplying all the probabilities with 1/p where p is the probability of moving to the given state and sets the probability of moving to the given state to zero. | |
std::size_t | size () const |
Retrieves the size of the distribution, i.e. | |
bool | less (Distribution< ValueType, StateType > const &other, storm::utility::ConstantsComparator< ValueType > const &comparator) const |
ValueType | getProbability (StateType const &state) const |
Returns the probability of the given state. | |
void | normalize () |
Normalizes the distribution such that the values sum up to one. | |
StateType | sampleFromDistribution (ValueType const &quantile) const |
Given a value q, find the event in the ordered distribution that corresponds to this prob. | |
Definition at line 16 of file Distribution.h.
typedef container_type::const_iterator storm::storage::Distribution< ValueType, StateType >::const_iterator |
Definition at line 20 of file Distribution.h.
typedef boost::container::flat_map<StateType, ValueType> storm::storage::Distribution< ValueType, StateType >::container_type |
Definition at line 18 of file Distribution.h.
typedef container_type::iterator storm::storage::Distribution< ValueType, StateType >::iterator |
Definition at line 19 of file Distribution.h.
storm::storage::Distribution< ValueType, StateType >::Distribution | ( | ) |
Creates an empty distribution.
Definition at line 17 of file Distribution.cpp.
|
default |
|
default |
void storm::storage::Distribution< ValueType, StateType >::add | ( | Distribution< ValueType, StateType > const & | other | ) |
Adds the given distribution to the current one.
Definition at line 27 of file Distribution.cpp.
void storm::storage::Distribution< ValueType, StateType >::addProbability | ( | StateType const & | state, |
ValueType const & | probability | ||
) |
Assigns the given state the given probability under this distribution.
state | The state to which to assign the probability. |
probability | The probability to assign. |
Definition at line 59 of file Distribution.cpp.
Distribution< ValueType, StateType >::iterator storm::storage::Distribution< ValueType, StateType >::begin | ( | ) |
Retrieves an iterator to the elements in this distribution.
Definition at line 82 of file Distribution.cpp.
Distribution< ValueType, StateType >::const_iterator storm::storage::Distribution< ValueType, StateType >::begin | ( | ) | const |
Retrieves an iterator to the elements in this distribution.
Definition at line 87 of file Distribution.cpp.
Distribution< ValueType, StateType >::const_iterator storm::storage::Distribution< ValueType, StateType >::cbegin | ( | ) | const |
Retrieves an iterator to the elements in this distribution.
Definition at line 92 of file Distribution.cpp.
Distribution< ValueType, StateType >::const_iterator storm::storage::Distribution< ValueType, StateType >::cend | ( | ) | const |
Retrieves an iterator past the elements in this distribution.
Definition at line 107 of file Distribution.cpp.
Distribution< ValueType, StateType >::iterator storm::storage::Distribution< ValueType, StateType >::end | ( | ) |
Retrieves an iterator past the elements in this distribution.
Definition at line 97 of file Distribution.cpp.
Distribution< ValueType, StateType >::const_iterator storm::storage::Distribution< ValueType, StateType >::end | ( | ) | const |
Retrieves an iterator past the elements in this distribution.
Definition at line 102 of file Distribution.cpp.
bool storm::storage::Distribution< ValueType, StateType >::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.
other | The distribution with which the current distribution is to be compared. |
Definition at line 35 of file Distribution.cpp.
ValueType storm::storage::Distribution< ValueType, StateType >::getProbability | ( | StateType const & | state | ) | const |
Returns the probability of the given state.
state | The state for which the probability is returned. |
Definition at line 164 of file Distribution.cpp.
bool storm::storage::Distribution< ValueType, StateType >::less | ( | Distribution< ValueType, StateType > const & | other, |
storm::utility::ConstantsComparator< ValueType > const & | comparator | ||
) | const |
Definition at line 141 of file Distribution.cpp.
void storm::storage::Distribution< ValueType, StateType >::normalize | ( | ) |
Normalizes the distribution such that the values sum up to one.
Definition at line 174 of file Distribution.cpp.
|
default |
|
default |
void storm::storage::Distribution< ValueType, StateType >::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.
state | The state for which to remove the probability. |
probability | The probability to remove. |
comparator | A comparator that is used to determine if the remaining probability is zero. If so, the entry is removed. |
Definition at line 64 of file Distribution.cpp.
void storm::storage::Distribution< ValueType, StateType >::reserve | ( | uint64_t | size | ) |
Definition at line 22 of file Distribution.cpp.
StateType storm::storage::Distribution< ValueType, StateType >::sampleFromDistribution | ( | ValueType const & | quantile | ) | const |
Given a value q, find the event in the ordered distribution that corresponds to this prob.
Example: Given a (sub)distribution { x -> 0.4, y -> 0.3, z -> 0.2 }, A value q in [0,0.4] yields x, q in [0.4, 0.7] yields y, and q in [0.7, 0.9] yields z. Any other value for q yields undefined behavior.
quantile | q, a value in the CDF. |
Definition at line 205 of file Distribution.cpp.
void storm::storage::Distribution< ValueType, StateType >::scale | ( | StateType const & | state | ) |
Scales the distribution by multiplying all the probabilities with 1/p where p is the probability of moving to the given state and sets the probability of moving to the given state to zero.
If the probability is already zero, this operation has no effect.
state | The state whose associated probability is used to scale the distribution. |
Definition at line 112 of file Distribution.cpp.
void storm::storage::Distribution< ValueType, StateType >::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.
fromState | The state from which to take the probability mass. |
toState | The state from which to which to add the probability mass. |
probability | The probability mass to shift. |
comparator | A comparator that is used to determine if the remaining probability is zero. If so, the entry is removed. |
Definition at line 75 of file Distribution.cpp.
std::size_t storm::storage::Distribution< ValueType, StateType >::size | ( | ) | const |
Retrieves the size of the distribution, i.e.
the size of the support set.
Definition at line 125 of file Distribution.cpp.