Storm
A Modern Probabilistic Model Checker
|
#include <SignatureComputer.h>
Public Member Functions | |
SignatureComputer (storm::models::symbolic::Model< DdType, ValueType > const &model, SignatureMode const &mode=SignatureMode::Eager, bool ensureQualitative=false) | |
SignatureComputer (storm::dd::Add< DdType, ValueType > const &transitionMatrix, std::set< storm::expressions::Variable > const &columnVariables, SignatureMode const &mode=SignatureMode::Eager, bool ensureQualitative=false) | |
SignatureComputer (storm::dd::Bdd< DdType > const &qualitativeTransitionMatrix, std::set< storm::expressions::Variable > const &columnVariables, SignatureMode const &mode=SignatureMode::Eager, bool ensureQualitative=false) | |
SignatureComputer (storm::dd::Add< DdType, ValueType > const &transitionMatrix, boost::optional< storm::dd::Bdd< DdType > > const &qualitativeTransitionMatrix, std::set< storm::expressions::Variable > const &columnVariables, SignatureMode const &mode=SignatureMode::Eager, bool ensureQualitative=false) | |
void | setSignatureMode (SignatureMode const &newMode) |
SignatureIterator< DdType, ValueType > | compute (Partition< DdType, ValueType > const &partition) |
Signature< DdType, ValueType > | getFullSignature (Partition< DdType, ValueType > const &partition) const |
Methods to compute the signatures. | |
Signature< DdType, ValueType > | getQualitativeSignature (Partition< DdType, ValueType > const &partition) const |
Friends | |
class | SignatureIterator< DdType, ValueType > |
Definition at line 41 of file SignatureComputer.h.
storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::SignatureComputer | ( | storm::models::symbolic::Model< DdType, ValueType > const & | model, |
SignatureMode const & | mode = SignatureMode::Eager , |
||
bool | ensureQualitative = false |
||
) |
Definition at line 65 of file SignatureComputer.cpp.
storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::SignatureComputer | ( | storm::dd::Add< DdType, ValueType > const & | transitionMatrix, |
std::set< storm::expressions::Variable > const & | columnVariables, | ||
SignatureMode const & | mode = SignatureMode::Eager , |
||
bool | ensureQualitative = false |
||
) |
Definition at line 72 of file SignatureComputer.cpp.
storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::SignatureComputer | ( | storm::dd::Bdd< DdType > const & | qualitativeTransitionMatrix, |
std::set< storm::expressions::Variable > const & | columnVariables, | ||
SignatureMode const & | mode = SignatureMode::Eager , |
||
bool | ensureQualitative = false |
||
) |
Definition at line 80 of file SignatureComputer.cpp.
storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::SignatureComputer | ( | storm::dd::Add< DdType, ValueType > const & | transitionMatrix, |
boost::optional< storm::dd::Bdd< DdType > > const & | qualitativeTransitionMatrix, | ||
std::set< storm::expressions::Variable > const & | columnVariables, | ||
SignatureMode const & | mode = SignatureMode::Eager , |
||
bool | ensureQualitative = false |
||
) |
Definition at line 88 of file SignatureComputer.cpp.
SignatureIterator< DdType, ValueType > storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::compute | ( | Partition< DdType, ValueType > const & | partition | ) |
Definition at line 108 of file SignatureComputer.cpp.
Signature< DdType, ValueType > storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::getFullSignature | ( | Partition< DdType, ValueType > const & | partition | ) | const |
Methods to compute the signatures.
Definition at line 123 of file SignatureComputer.cpp.
Signature< DdType, ValueType > storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::getQualitativeSignature | ( | Partition< DdType, ValueType > const & | partition | ) | const |
Definition at line 140 of file SignatureComputer.cpp.
void storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::setSignatureMode | ( | SignatureMode const & | newMode | ) |
Definition at line 113 of file SignatureComputer.cpp.
|
friend |
Definition at line 37 of file SignatureComputer.h.