Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm::dd::bisimulation::SignatureComputer< DdType, ValueType > Class Template Reference

#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 >
 

Detailed Description

template<storm::dd::DdType DdType, typename ValueType>
class storm::dd::bisimulation::SignatureComputer< DdType, ValueType >

Definition at line 41 of file SignatureComputer.h.

Constructor & Destructor Documentation

◆ SignatureComputer() [1/4]

template<storm::dd::DdType DdType, typename ValueType >
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.

◆ SignatureComputer() [2/4]

template<storm::dd::DdType DdType, typename ValueType >
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.

◆ SignatureComputer() [3/4]

template<storm::dd::DdType DdType, typename ValueType >
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.

◆ SignatureComputer() [4/4]

template<storm::dd::DdType DdType, typename ValueType >
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.

Member Function Documentation

◆ compute()

template<storm::dd::DdType DdType, typename ValueType >
SignatureIterator< DdType, ValueType > storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::compute ( Partition< DdType, ValueType > const &  partition)

Definition at line 108 of file SignatureComputer.cpp.

◆ getFullSignature()

template<storm::dd::DdType DdType, typename ValueType >
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.

◆ getQualitativeSignature()

template<storm::dd::DdType DdType, typename ValueType >
Signature< DdType, ValueType > storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::getQualitativeSignature ( Partition< DdType, ValueType > const &  partition) const

Definition at line 140 of file SignatureComputer.cpp.

◆ setSignatureMode()

template<storm::dd::DdType DdType, typename ValueType >
void storm::dd::bisimulation::SignatureComputer< DdType, ValueType >::setSignatureMode ( SignatureMode const &  newMode)

Definition at line 113 of file SignatureComputer.cpp.

Friends And Related Symbol Documentation

◆ SignatureIterator< DdType, ValueType >

template<storm::dd::DdType DdType, typename ValueType >
friend class SignatureIterator< DdType, ValueType >
friend

Definition at line 37 of file SignatureComputer.h.


The documentation for this class was generated from the following files: