Storm
A Modern Probabilistic Model Checker
|
#include <Add.h>
Classes | |
struct | MatrixAndLabeling |
Converts the ADD to a row-grouped (sparse) matrix. More... | |
Public Member Functions | |
Add ()=default | |
Add (Add< LibraryType, ValueType > const &other)=default | |
Add & | operator= (Add< LibraryType, ValueType > const &other)=default |
Add (Add< LibraryType, ValueType > &&other)=default | |
Add & | operator= (Add< LibraryType, ValueType > &&other)=default |
bool | operator== (Add< LibraryType, ValueType > const &other) const |
Retrieves whether the two DDs represent the same function. | |
bool | operator!= (Add< LibraryType, ValueType > const &other) const |
Retrieves whether the two DDs represent different functions. | |
Add< LibraryType, ValueType > | operator+ (Add< LibraryType, ValueType > const &other) const |
Adds the two ADDs. | |
Add< LibraryType, ValueType > & | operator+= (Add< LibraryType, ValueType > const &other) |
Adds the given ADD to the current one. | |
Add< LibraryType, ValueType > | operator* (Add< LibraryType, ValueType > const &other) const |
Multiplies the two ADDs. | |
Add< LibraryType, ValueType > & | operator*= (Add< LibraryType, ValueType > const &other) |
Multiplies the given ADD with the current one and assigns the result to the current ADD. | |
Add< LibraryType, ValueType > | operator- (Add< LibraryType, ValueType > const &other) const |
Subtracts the given ADD from the current one. | |
Add< LibraryType, ValueType > | operator- () const |
Subtracts the ADD from the constant zero function. | |
Add< LibraryType, ValueType > & | operator-= (Add< LibraryType, ValueType > const &other) |
Subtracts the given ADD from the current one and assigns the result to the current ADD. | |
Add< LibraryType, ValueType > | operator/ (Add< LibraryType, ValueType > const &other) const |
Divides the current ADD by the given one. | |
Add< LibraryType, ValueType > & | operator/= (Add< LibraryType, ValueType > const &other) |
Divides the current ADD by the given one and assigns the result to the current ADD. | |
Bdd< LibraryType > | equals (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that maps all evaluations to one that have identical function values. | |
Bdd< LibraryType > | notEquals (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that maps all evaluations to one that have distinct function values. | |
Bdd< LibraryType > | less (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that maps all evaluations to one whose function value in the first ADD are less than the one in the given ADD. | |
Bdd< LibraryType > | lessOrEqual (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or equal than the one in the given ADD. | |
Bdd< LibraryType > | greater (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater than the one in the given ADD. | |
Bdd< LibraryType > | greaterOrEqual (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater or equal than the one in the given ADD. | |
Add< LibraryType, ValueType > | pow (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that represents the current ADD to the power of the given ADD. | |
Add< LibraryType, ValueType > | mod (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that represents the current ADD modulo the given ADD. | |
Add< LibraryType, ValueType > | logxy (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that represents the logarithm of the current ADD to the bases given by the second ADD. | |
Add< LibraryType, ValueType > | floor () const |
Retrieves the function that floors all values in the current ADD. | |
Add< LibraryType, ValueType > | ceil () const |
Retrieves the function that ceils all values in the current ADD. | |
Add< LibraryType, storm::RationalNumber > | sharpenKwekMehlhorn (uint64_t precision) const |
Retrieves the function that sharpens all values in the current ADD with the Kwek-Mehlhorn algorithm. | |
Add< LibraryType, ValueType > | minimum (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that maps all evaluations to the minimum of the function values of the two ADDs. | |
Add< LibraryType, ValueType > | maximum (Add< LibraryType, ValueType > const &other) const |
Retrieves the function that maps all evaluations to the maximum of the function values of the two ADDs. | |
template<typename TargetValueType > | |
std::enable_if< std::is_same< TargetValueType, ValueType >::value, Add< LibraryType, TargetValueType > >::type | toValueType () const |
Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else. | |
template<typename TargetValueType > | |
std::enable_if<!std::is_same< TargetValueType, ValueType >::value, Add< LibraryType, TargetValueType > >::type | toValueType () const |
Add< LibraryType, ValueType > | sumAbstract (std::set< storm::expressions::Variable > const &metaVariables) const |
Sum-abstracts from the given meta variables. | |
Add< LibraryType, ValueType > | minAbstract (std::set< storm::expressions::Variable > const &metaVariables) const |
Min-abstracts from the given meta variables. | |
Bdd< LibraryType > | minAbstractRepresentative (std::set< storm::expressions::Variable > const &metaVariables) const |
Similar to minAbstract , but does not abstract from the variables but rather picks a valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a valuation (of the other variables) that make the function evaluate to the minimal value. | |
Add< LibraryType, ValueType > | maxAbstract (std::set< storm::expressions::Variable > const &metaVariables) const |
Max-abstracts from the given meta variables. | |
Bdd< LibraryType > | maxAbstractRepresentative (std::set< storm::expressions::Variable > const &metaVariables) const |
Similar to maxAbstract , but does not abstract from the variables but rather picks a valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a valuation (of the other variables) that make the function evaluate to the maximal value. | |
bool | equalModuloPrecision (Add< LibraryType, ValueType > const &other, ValueType const &precision, bool relative=true) const |
Checks whether the current and the given ADD represent the same function modulo some given precision. | |
Add< LibraryType, ValueType > | renameVariables (std::set< storm::expressions::Variable > const &from, std::set< storm::expressions::Variable > const &to) const |
Renames the given meta variables in the ADD. | |
Add< LibraryType, ValueType > | renameVariablesAbstract (std::set< storm::expressions::Variable > const &from, std::set< storm::expressions::Variable > const &to) const |
Renames the given meta variables in the ADD. | |
Add< LibraryType, ValueType > | swapVariables (std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const |
Swaps the given pairs of meta variables in the ADD. | |
Add< LibraryType, ValueType > | permuteVariables (std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const |
Permutes the given pairs of meta variables in the ADD. | |
Add< LibraryType, ValueType > | multiplyMatrix (Add< LibraryType, ValueType > const &otherMatrix, std::set< storm::expressions::Variable > const &summationMetaVariables) const |
Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta variables. | |
Add< LibraryType, ValueType > | multiplyMatrix (Bdd< LibraryType > const &otherMatrix, std::set< storm::expressions::Variable > const &summationMetaVariables) const |
Multiplies the current ADD (representing a matrix) with the given matrix (given by a BDD) by summing over the given meta variables. | |
Bdd< LibraryType > | greater (ValueType const &value) const |
Computes a BDD that represents the function in which all assignments with a function value strictly larger than the given value are mapped to one and all others to zero. | |
Bdd< LibraryType > | greaterOrEqual (ValueType const &value) const |
Computes a BDD that represents the function in which all assignments with a function value larger or equal to the given value are mapped to one and all others to zero. | |
Bdd< LibraryType > | less (ValueType const &value) const |
Computes a BDD that represents the function in which all assignments with a function value strictly lower than the given value are mapped to one and all others to zero. | |
Bdd< LibraryType > | lessOrEqual (ValueType const &value) const |
Computes a BDD that represents the function in which all assignments with a function value less or equal to the given value are mapped to one and all others to zero. | |
Bdd< LibraryType > | notZero () const |
Computes a BDD that represents the function in which all assignments with a function value unequal to zero are mapped to one and all others to zero. | |
Add< LibraryType, ValueType > | constrain (Add< LibraryType, ValueType > const &constraint) const |
Computes the constraint of the current ADD with the given constraint. | |
Add< LibraryType, ValueType > | restrict (Add< LibraryType, ValueType > const &constraint) const |
Computes the restriction of the current ADD with the given constraint. | |
Bdd< LibraryType > | getSupport () const override |
Retrieves the support of the current ADD. | |
virtual uint_fast64_t | getNonZeroCount () const override |
Retrieves the number of encodings that are mapped to a non-zero value. | |
virtual uint_fast64_t | getLeafCount () const override |
Retrieves the number of leaves of the ADD. | |
virtual uint_fast64_t | getNodeCount () const override |
Retrieves the number of nodes necessary to represent the DD. | |
ValueType | getMin () const |
Retrieves the lowest function value of any encoding. | |
ValueType | getMax () const |
Retrieves the highest function value of any encoding. | |
void | setValue (storm::expressions::Variable const &metaVariable, int_fast64_t variableValue, ValueType const &targetValue) |
Sets the function values of all encodings that have the given value of the meta variable to the given target value. | |
void | setValue (storm::expressions::Variable const &metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const &metaVariable2, int_fast64_t variableValue2, ValueType const &targetValue) |
Sets the function values of all encodings that have the given values of the two meta variables to the given target value. | |
void | setValue (std::map< storm::expressions::Variable, int_fast64_t > const &metaVariableToValueMap=std::map< storm::expressions::Variable, int_fast64_t >(), ValueType const &targetValue=0) |
Sets the function values of all encodings that have the given values of the given meta variables to the given target value. | |
ValueType | getValue (std::map< storm::expressions::Variable, int_fast64_t > const &metaVariableToValueMap=std::map< storm::expressions::Variable, int_fast64_t >()) const |
Retrieves the value of the function when all meta variables are assigned the values of the given mapping. | |
bool | isOne () const |
Retrieves whether this ADD represents the constant one function. | |
bool | isZero () const |
Retrieves whether this ADD represents the constant zero function. | |
bool | isConstant () const |
Retrieves whether this ADD represents a constant function. | |
virtual uint_fast64_t | getIndex () const override |
Retrieves the index of the topmost variable in the DD. | |
virtual uint_fast64_t | getLevel () const override |
Retrieves the level of the topmost variable in the DD. | |
std::vector< ValueType > | toVector () const |
Converts the ADD to a vector. | |
std::vector< ValueType > | toVector (storm::dd::Odd const &rowOdd) const |
Converts the ADD to a vector. | |
std::vector< ValueType > | toVector (storm::dd::Add< LibraryType, ValueType > const &matrix, std::vector< uint_fast64_t > const &rowGroupIndices, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd) const |
Converts the ADD to a row-grouped vector while respecting the row group sizes of the provided matrix. | |
storm::storage::SparseMatrix< ValueType > | toMatrix () const |
Converts the ADD to a (sparse) matrix. | |
storm::storage::SparseMatrix< ValueType > | toMatrix (storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const |
Converts the ADD to a (sparse) matrix. | |
storm::storage::SparseMatrix< ValueType > | toMatrix (std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const |
Converts the ADD to a (sparse) matrix. | |
storm::storage::SparseMatrix< ValueType > | toMatrix (std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const |
Converts the ADD to a row-grouped (sparse) matrix. | |
MatrixAndLabeling | toLabeledMatrix (std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd, std::vector< std::set< storm::expressions::Variable > > const &labelMetaVariables=std::vector< std::set< storm::expressions::Variable > >()) const |
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > | toMatrixVector (storm::dd::Add< LibraryType, ValueType > const &vector, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const |
Converts the ADD to a row-grouped (sparse) matrix and the given vector to a row-grouped vector. | |
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > | toMatrixVector (std::vector< uint_fast64_t > &&rowGroupSizes, storm::dd::Add< LibraryType, ValueType > const &vector, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const |
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< std::vector< ValueType > > > | toMatrixVectors (std::vector< storm::dd::Add< LibraryType, ValueType > > const &vectors, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const |
Converts the ADD to a row-grouped (sparse) matrix and the given vectors to row-grouped vectors. | |
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< std::vector< ValueType > > > | toMatrixVectors (std::vector< uint_fast64_t > &&rowGroupSizes, std::vector< storm::dd::Add< LibraryType, ValueType > > const &vectors, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const |
void | exportToDot (std::string const &filename, bool showVariablesIfPossible=true) const override |
Exports the DD to the given file in the dot format. | |
virtual void | exportToText (std::string const &filename) const override |
Exports the DD to the given file in the dot format. | |
AddIterator< LibraryType, ValueType > | begin (bool enumerateDontCareMetaVariables=true) const |
Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. | |
AddIterator< LibraryType, ValueType > | end () const |
Retrieves an iterator that points past the end of the container. | |
Bdd< LibraryType > | toBdd () const |
Converts the ADD to a BDD by mapping all values unequal to zero to 1. | |
Odd | createOdd () const |
Creates an ODD based on the current ADD. | |
InternalAdd< LibraryType, ValueType > const & | getInternalAdd () const |
Retrieves the internal ADD. | |
InternalDdManager< LibraryType > const & | getInternalDdManager () const |
Retrieves the internal ADD. | |
Add< storm::dd::DdType::Sylvan, storm::RationalNumber > | sharpenKwekMehlhorn (uint64_t precision) const |
Add< storm::dd::DdType::Sylvan, storm::RationalNumber > | sharpenKwekMehlhorn (uint64_t precision) const |
![]() | |
Dd ()=default | |
Dd (Dd< LibraryType > const &other)=default | |
Dd & | operator= (Dd< LibraryType > const &other)=default |
Dd (Dd< LibraryType > &&other)=default | |
Dd & | operator= (Dd< LibraryType > &&other)=default |
virtual | ~Dd ()=default |
bool | containsMetaVariable (storm::expressions::Variable const &metaVariable) const |
Retrieves whether the given meta variable is contained in the DD. | |
bool | containsMetaVariables (std::set< storm::expressions::Variable > const &metaVariables) const |
Retrieves whether the given meta variables are all contained in the DD. | |
std::set< storm::expressions::Variable > const & | getContainedMetaVariables () const |
Retrieves the set of all meta variables contained in the DD. | |
DdManager< LibraryType > & | getDdManager () const |
Retrieves the manager that is responsible for this DD. | |
std::set< storm::expressions::Variable > & | getContainedMetaVariables () |
Retrieves the set of all meta variables contained in the DD. | |
void | addMetaVariables (std::set< storm::expressions::Variable > const &metaVariables) |
Adds the given set of meta variables to the DD. | |
void | addMetaVariable (storm::expressions::Variable const &metaVariable) |
Adds the given meta variable to the set of meta variables that are contained in this DD. | |
void | removeMetaVariable (storm::expressions::Variable const &metaVariable) |
Removes the given meta variable to the set of meta variables that are contained in this DD. | |
void | removeMetaVariables (std::set< storm::expressions::Variable > const &metaVariables) |
Removes the given set of meta variables from the DD. | |
Static Public Member Functions | |
static Add< LibraryType, ValueType > | fromVector (DdManager< LibraryType > const &ddManager, std::vector< ValueType > const &values, Odd const &odd, std::set< storm::expressions::Variable > const &metaVariables) |
Builds an ADD representing the given vector. | |
Friends | |
class | DdManager< LibraryType > |
class | Bdd< LibraryType > |
template<DdType LibraryTypePrime, typename ValueTypePrime > | |
class | Add |
class | bisimulation::InternalSignatureRefiner< LibraryType, ValueType > |
template<DdType LibraryTypePrime, typename ValueTypePrime > | |
std::ostream & | operator<< (std::ostream &out, Add< LibraryTypePrime, ValueTypePrime > const &add) |
Additional Inherited Members | |
![]() | |
std::vector< uint_fast64_t > | getSortedVariableIndices () const |
Retrieves the (sorted) list of the variable indices of DD variables contained in this DD. | |
Dd (DdManager< LibraryType > const &ddManager, std::set< storm::expressions::Variable > const &containedMetaVariables=std::set< storm::expressions::Variable >()) | |
Creates a DD with the given manager and meta variables. | |
![]() | |
static std::set< storm::expressions::Variable > | joinMetaVariables (storm::dd::Dd< LibraryType > const &first, storm::dd::Dd< LibraryType > const &second) |
Retrieves the set of meta variables contained in both DDs. | |
static std::set< storm::expressions::Variable > | subtractMetaVariables (storm::dd::Dd< LibraryType > const &first, storm::dd::Dd< LibraryType > const &second) |
Retrieves the set of meta variables that are contained in the first but not the second DD. | |
|
default |
|
default |
|
default |
AddIterator< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::begin | ( | bool | enumerateDontCareMetaVariables = true | ) | const |
Retrieves an iterator that points to the first meta variable assignment with a non-zero function value.
enumerateDontCareMetaVariables | If set to true, all meta variable assignments are enumerated, even if a meta variable does not at all influence the the function value. |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::ceil | ( | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::constrain | ( | Add< LibraryType, ValueType > const & | constraint | ) | const |
Computes the constraint of the current ADD with the given constraint.
That is, the function value of the resulting ADD will be the same as the current ones for all assignments mapping to one in the constraint and may be different otherwise.
constraint | The constraint to use for the operation. |
Odd storm::dd::Add< LibraryType, ValueType >::createOdd | ( | ) | const |
AddIterator< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::end | ( | ) | const |
bool storm::dd::Add< LibraryType, ValueType >::equalModuloPrecision | ( | Add< LibraryType, ValueType > const & | other, |
ValueType const & | precision, | ||
bool | relative = true |
||
) | const |
Checks whether the current and the given ADD represent the same function modulo some given precision.
other | The ADD with which to compare. |
precision | An upper bound on the maximal difference between any two function values that is to be tolerated. |
relative | If set to true, not the absolute values have to be within the precision, but the relative values. |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::equals | ( | Add< LibraryType, ValueType > const & | other | ) | const |
|
overridevirtual |
Exports the DD to the given file in the dot format.
filename | The name of the file to which the DD is to be exported. |
Implements storm::dd::Dd< LibraryType >.
|
overridevirtual |
Exports the DD to the given file in the dot format.
filename | The name of the file to which the DD is to be exported. |
Implements storm::dd::Dd< LibraryType >.
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::floor | ( | ) | const |
|
static |
Builds an ADD representing the given vector.
ddManager | The manager responsible for the ADD. |
values | The vector that is to be represented by the ADD. |
odd | The ODD used for the translation. |
metaVariables | The meta variables used for the translation. |
|
overridevirtual |
Retrieves the index of the topmost variable in the DD.
Implements storm::dd::Dd< LibraryType >.
InternalAdd< LibraryType, ValueType > const & storm::dd::Add< LibraryType, ValueType >::getInternalAdd | ( | ) | const |
InternalDdManager< LibraryType > const & storm::dd::Add< LibraryType, ValueType >::getInternalDdManager | ( | ) | const |
|
overridevirtual |
Retrieves the number of leaves of the ADD.
Implements storm::dd::Dd< LibraryType >.
|
overridevirtual |
Retrieves the level of the topmost variable in the DD.
Implements storm::dd::Dd< LibraryType >.
ValueType storm::dd::Add< LibraryType, ValueType >::getMax | ( | ) | const |
ValueType storm::dd::Add< LibraryType, ValueType >::getMin | ( | ) | const |
|
overridevirtual |
Retrieves the number of nodes necessary to represent the DD.
Implements storm::dd::Dd< LibraryType >.
|
overridevirtual |
Retrieves the number of encodings that are mapped to a non-zero value.
Implements storm::dd::Dd< LibraryType >.
|
overridevirtual |
Retrieves the support of the current ADD.
Implements storm::dd::Dd< LibraryType >.
ValueType storm::dd::Add< LibraryType, ValueType >::getValue | ( | std::map< storm::expressions::Variable, int_fast64_t > const & | metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>() | ) | const |
Retrieves the value of the function when all meta variables are assigned the values of the given mapping.
Note that the mapping must specify values for all meta variables contained in the DD.
metaVariableToValueMap | A mapping of meta variables to their values. |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::greater | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::greater | ( | ValueType const & | value | ) | const |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::greaterOrEqual | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::greaterOrEqual | ( | ValueType const & | value | ) | const |
bool storm::dd::Add< LibraryType, ValueType >::isConstant | ( | ) | const |
bool storm::dd::Add< LibraryType, ValueType >::isOne | ( | ) | const |
bool storm::dd::Add< LibraryType, ValueType >::isZero | ( | ) | const |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::less | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::less | ( | ValueType const & | value | ) | const |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::lessOrEqual | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::lessOrEqual | ( | ValueType const & | value | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::logxy | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::maxAbstract | ( | std::set< storm::expressions::Variable > const & | metaVariables | ) | const |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::maxAbstractRepresentative | ( | std::set< storm::expressions::Variable > const & | metaVariables | ) | const |
Similar to maxAbstract
, but does not abstract from the variables but rather picks a valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a valuation (of the other variables) that make the function evaluate to the maximal value.
metaVariables | The meta variables from which to abstract. |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::maximum | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::minAbstract | ( | std::set< storm::expressions::Variable > const & | metaVariables | ) | const |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::minAbstractRepresentative | ( | std::set< storm::expressions::Variable > const & | metaVariables | ) | const |
Similar to minAbstract
, but does not abstract from the variables but rather picks a valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a valuation (of the other variables) that make the function evaluate to the minimal value.
metaVariables | The meta variables from which to abstract. |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::minimum | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::mod | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::multiplyMatrix | ( | Add< LibraryType, ValueType > const & | otherMatrix, |
std::set< storm::expressions::Variable > const & | summationMetaVariables | ||
) | const |
Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta variables.
otherMatrix | The matrix with which to multiply. |
summationMetaVariables | The names of the meta variables over which to sum during the matrix- matrix multiplication. |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::multiplyMatrix | ( | Bdd< LibraryType > const & | otherMatrix, |
std::set< storm::expressions::Variable > const & | summationMetaVariables | ||
) | const |
Multiplies the current ADD (representing a matrix) with the given matrix (given by a BDD) by summing over the given meta variables.
otherMatrix | The matrix with which to multiply. |
summationMetaVariables | The names of the meta variables over which to sum during the matrix- matrix multiplication. |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::notEquals | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::notZero | ( | ) | const |
bool storm::dd::Add< LibraryType, ValueType >::operator!= | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::operator* | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > & storm::dd::Add< LibraryType, ValueType >::operator*= | ( | Add< LibraryType, ValueType > const & | other | ) |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::operator+ | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > & storm::dd::Add< LibraryType, ValueType >::operator+= | ( | Add< LibraryType, ValueType > const & | other | ) |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::operator- | ( | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::operator- | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > & storm::dd::Add< LibraryType, ValueType >::operator-= | ( | Add< LibraryType, ValueType > const & | other | ) |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::operator/ | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > & storm::dd::Add< LibraryType, ValueType >::operator/= | ( | Add< LibraryType, ValueType > const & | other | ) |
|
default |
|
default |
bool storm::dd::Add< LibraryType, ValueType >::operator== | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::permuteVariables | ( | std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & | metaVariablePairs | ) | const |
Permutes the given pairs of meta variables in the ADD.
The pairs of meta variables must be guaranteed to have the same number of underlying ADD variables. The first component of the i-th entry is substituted by the second component.
metaVariablePairs | A vector of meta variable pairs that are to be permuted. |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::pow | ( | Add< LibraryType, ValueType > const & | other | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::renameVariables | ( | std::set< storm::expressions::Variable > const & | from, |
std::set< storm::expressions::Variable > const & | to | ||
) | const |
Renames the given meta variables in the ADD.
The number of the underlying DD variables of the both meta variable sets needs to agree.
from | The meta variables to be renamed. The current ADD needs to contain all these meta variables. |
to | The meta variables that are the target of the renaming process. The current ADD must not contain any of these meta variables. |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::renameVariablesAbstract | ( | std::set< storm::expressions::Variable > const & | from, |
std::set< storm::expressions::Variable > const & | to | ||
) | const |
Renames the given meta variables in the ADD.
The number of the underlying DD variables of the from meta variable set needs to be at least as large as the to meta variable set. If the amount of variables coincide, this operation coincides with renameVariables. Otherwise, it first abstracts from the superfluous variables and then performs the renaming.
from | The meta variables to be renamed. The current ADD needs to contain all these meta variables. |
to | The meta variables that are the target of the renaming process. The current ADD must not contain any of these meta variables. |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::restrict | ( | Add< LibraryType, ValueType > const & | constraint | ) | const |
Computes the restriction of the current ADD with the given constraint.
That is, the function value of the resulting DD will be the same as the current ones for all assignments mapping to one in the constraint and may be different otherwise.
constraint | The constraint to use for the operation. |
void storm::dd::Add< LibraryType, ValueType >::setValue | ( | std::map< storm::expressions::Variable, int_fast64_t > const & | metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>() , |
ValueType const & | targetValue = 0 |
||
) |
Sets the function values of all encodings that have the given values of the given meta variables to the given target value.
metaVariableToValueMap | A mapping of meta variables to the values they are supposed to have. All values must be within the range of the respective meta variable. |
targetValue | The new function value of the modified encodings. |
void storm::dd::Add< LibraryType, ValueType >::setValue | ( | storm::expressions::Variable const & | metaVariable, |
int_fast64_t | variableValue, | ||
ValueType const & | targetValue | ||
) |
Sets the function values of all encodings that have the given value of the meta variable to the given target value.
metaVariable | The meta variable that has to be equal to the given value. |
variableValue | The value that the meta variable is supposed to have. This must be within the range of the meta variable. |
targetValue | The new function value of the modified encodings. |
void storm::dd::Add< LibraryType, ValueType >::setValue | ( | storm::expressions::Variable const & | metaVariable1, |
int_fast64_t | variableValue1, | ||
storm::expressions::Variable const & | metaVariable2, | ||
int_fast64_t | variableValue2, | ||
ValueType const & | targetValue | ||
) |
Sets the function values of all encodings that have the given values of the two meta variables to the given target value.
metaVariable1 | The first meta variable that has to be equal to the first given value. |
variableValue1 | The value that the first meta variable is supposed to have. This must be within the range of the meta variable. |
metaVariable2 | The second meta variable that has to be equal to the second given value. |
variableValue2 | The value that the second meta variable is supposed to have. This must be within the range of the meta variable. |
targetValue | The new function value of the modified encodings. |
Add< storm::dd::DdType::Sylvan, storm::RationalNumber > storm::dd::Add< storm::dd::DdType::Sylvan, double >::sharpenKwekMehlhorn | ( | uint64_t | precision | ) | const |
Add< storm::dd::DdType::Sylvan, storm::RationalNumber > storm::dd::Add< storm::dd::DdType::Sylvan, storm::RationalNumber >::sharpenKwekMehlhorn | ( | uint64_t | precision | ) | const |
Add< LibraryType, storm::RationalNumber > storm::dd::Add< LibraryType, ValueType >::sharpenKwekMehlhorn | ( | uint64_t | precision | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::sumAbstract | ( | std::set< storm::expressions::Variable > const & | metaVariables | ) | const |
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::swapVariables | ( | std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & | metaVariablePairs | ) | const |
Swaps the given pairs of meta variables in the ADD.
The pairs of meta variables must be guaranteed to have the same number of underlying ADD variables.
metaVariablePairs | A vector of meta variable pairs that are to be swapped for one another. |
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::toBdd | ( | ) | const |
Add< LibraryType, ValueType >::MatrixAndLabeling storm::dd::Add< LibraryType, ValueType >::toLabeledMatrix | ( | std::set< storm::expressions::Variable > const & | rowMetaVariables, |
std::set< storm::expressions::Variable > const & | columnMetaVariables, | ||
std::set< storm::expressions::Variable > const & | groupMetaVariables, | ||
storm::dd::Odd const & | rowOdd, | ||
storm::dd::Odd const & | columnOdd, | ||
std::vector< std::set< storm::expressions::Variable > > const & | labelMetaVariables = std::vector<std::set<storm::expressions::Variable>>() |
||
) | const |
storm::storage::SparseMatrix< ValueType > storm::dd::Add< LibraryType, ValueType >::toMatrix | ( | ) | const |
storm::storage::SparseMatrix< ValueType > storm::dd::Add< LibraryType, ValueType >::toMatrix | ( | std::set< storm::expressions::Variable > const & | groupMetaVariables, |
storm::dd::Odd const & | rowOdd, | ||
storm::dd::Odd const & | columnOdd | ||
) | const |
Converts the ADD to a row-grouped (sparse) matrix.
The given offset-labeled DDs are used to determine the correct row and column, respectively, for each entry. Note: this function assumes that the meta variables used to distinguish different row groups are at the very top of the ADD.
groupMetaVariables | The meta variables that are used to distinguish different row groups. |
rowOdd | The ODD used for determining the correct row. |
columnOdd | The ODD used for determining the correct column. |
storm::storage::SparseMatrix< ValueType > storm::dd::Add< LibraryType, ValueType >::toMatrix | ( | std::set< storm::expressions::Variable > const & | rowMetaVariables, |
std::set< storm::expressions::Variable > const & | columnMetaVariables, | ||
storm::dd::Odd const & | rowOdd, | ||
storm::dd::Odd const & | columnOdd | ||
) | const |
Converts the ADD to a (sparse) matrix.
The given offset-labeled DDs are used to determine the correct row and column, respectively, for each entry.
rowMetaVariables | The meta variables that encode the rows of the matrix. |
columnMetaVariables | The meta variables that encode the columns of the matrix. |
rowOdd | The ODD used for determining the correct row. |
columnOdd | The ODD used for determining the correct column. |
storm::storage::SparseMatrix< ValueType > storm::dd::Add< LibraryType, ValueType >::toMatrix | ( | storm::dd::Odd const & | rowOdd, |
storm::dd::Odd const & | columnOdd | ||
) | const |
Converts the ADD to a (sparse) matrix.
All contained non-primed variables are assumed to encode the row, whereas all primed variables are assumed to encode the column. The given offset-labeled DDs are used to determine the correct row and column, respectively, for each entry.
rowOdd | The ODD used for determining the correct row. |
columnOdd | The ODD used for determining the correct column. |
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > storm::dd::Add< LibraryType, ValueType >::toMatrixVector | ( | std::vector< uint_fast64_t > && | rowGroupSizes, |
storm::dd::Add< LibraryType, ValueType > const & | vector, | ||
std::set< storm::expressions::Variable > const & | rowMetaVariables, | ||
std::set< storm::expressions::Variable > const & | columnMetaVariables, | ||
std::set< storm::expressions::Variable > const & | groupMetaVariables, | ||
storm::dd::Odd const & | rowOdd, | ||
storm::dd::Odd const & | columnOdd | ||
) | const |
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > storm::dd::Add< LibraryType, ValueType >::toMatrixVector | ( | storm::dd::Add< LibraryType, ValueType > const & | vector, |
std::set< storm::expressions::Variable > const & | groupMetaVariables, | ||
storm::dd::Odd const & | rowOdd, | ||
storm::dd::Odd const & | columnOdd | ||
) | const |
Converts the ADD to a row-grouped (sparse) matrix and the given vector to a row-grouped vector.
The given offset-labeled DDs are used to determine the correct row and column, respectively, for each entry. Note: this function assumes that the meta variables used to distinguish different row groups are at the very top of the ADD.
vector | The symbolic vector to convert. |
groupMetaVariables | The meta variables that are used to distinguish different row groups. |
rowOdd | The ODD used for determining the correct row. |
columnOdd | The ODD used for determining the correct column. |
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< std::vector< ValueType > > > storm::dd::Add< LibraryType, ValueType >::toMatrixVectors | ( | std::vector< storm::dd::Add< LibraryType, ValueType > > const & | vectors, |
std::set< storm::expressions::Variable > const & | groupMetaVariables, | ||
storm::dd::Odd const & | rowOdd, | ||
storm::dd::Odd const & | columnOdd | ||
) | const |
Converts the ADD to a row-grouped (sparse) matrix and the given vectors to row-grouped vectors.
The given offset-labeled DDs are used to determine the correct row and column, respectively, for each entry. Note: this function assumes that the meta variables used to distinguish different row groups are at the very top of the ADD.
vectors | The symbolic vectors to convert. |
groupMetaVariables | The meta variables that are used to distinguish different row groups. |
rowOdd | The ODD used for determining the correct row. |
columnOdd | The ODD used for determining the correct column. |
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< std::vector< ValueType > > > storm::dd::Add< LibraryType, ValueType >::toMatrixVectors | ( | std::vector< uint_fast64_t > && | rowGroupSizes, |
std::vector< storm::dd::Add< LibraryType, ValueType > > const & | vectors, | ||
std::set< storm::expressions::Variable > const & | rowMetaVariables, | ||
std::set< storm::expressions::Variable > const & | columnMetaVariables, | ||
std::set< storm::expressions::Variable > const & | groupMetaVariables, | ||
storm::dd::Odd const & | rowOdd, | ||
storm::dd::Odd const & | columnOdd | ||
) | const |
std::enable_if<!std::is_same< TargetValueType, ValueType >::value, Add< LibraryType, TargetValueType > >::type storm::dd::Add< LibraryType, ValueType >::toValueType | ( | ) | const |
std::enable_if<!std::is_same< TargetValueType, ValueType >::value, Add< LibraryType, TargetValueType > >::type storm::dd::Add< LibraryType, ValueType >::toValueType | ( | ) | const |
std::vector< ValueType > storm::dd::Add< LibraryType, ValueType >::toVector | ( | ) | const |
std::vector< ValueType > storm::dd::Add< LibraryType, ValueType >::toVector | ( | storm::dd::Add< LibraryType, ValueType > const & | matrix, |
std::vector< uint_fast64_t > const & | rowGroupIndices, | ||
std::set< storm::expressions::Variable > const & | rowMetaVariables, | ||
std::set< storm::expressions::Variable > const & | columnMetaVariables, | ||
std::set< storm::expressions::Variable > const & | groupMetaVariables, | ||
storm::dd::Odd const & | rowOdd | ||
) | const |
Converts the ADD to a row-grouped vector while respecting the row group sizes of the provided matrix.
That is, if the vector has a zero entry for some row in a row group for which the matrix has a non-zero row, the value at the vector will be correctly set to zero.
matrix | The symbolic matrix whose row group sizes to respect. |
rowGroupIndices | A vector specifying the sizes of the row groups. |
rowMetaVariables | The meta variables that encode the rows of the matrix. |
columnMetaVariables | The meta variables that encode the columns of the matrix. |
groupMetaVariables | The meta variables that are used to distinguish different row groups. |
rowOdd | The ODD used for determining the correct row. |
std::vector< ValueType > storm::dd::Add< LibraryType, ValueType >::toVector | ( | storm::dd::Odd const & | rowOdd | ) | const |
|
friend |
|
friend |