Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
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.

◆ 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: