Storm 1.10.0.1
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 85 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 90 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 95 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 110 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 100 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 105 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 167 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 144 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 177 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 67 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 208 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 115 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 78 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 128 of file Distribution.cpp.