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

#include <SignatureRefiner.h>

Public Member Functions

 SignatureRefiner (storm::dd::DdManager< DdType > const &manager, storm::expressions::Variable const &blockVariable, std::set< storm::expressions::Variable > const &stateRowVariables, std::set< storm::expressions::Variable > const &stateColumnVariables, bool shiftStateVariables, std::set< storm::expressions::Variable > const &nondeterminismVariables=std::set< storm::expressions::Variable >())
 
Partition< DdType, ValueType > refine (Partition< DdType, ValueType > const &oldPartition, Signature< DdType, ValueType > const &signature)
 

Detailed Description

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

Definition at line 18 of file SignatureRefiner.h.

Constructor & Destructor Documentation

◆ SignatureRefiner()

template<storm::dd::DdType DdType, typename ValueType >
storm::dd::bisimulation::SignatureRefiner< DdType, ValueType >::SignatureRefiner ( storm::dd::DdManager< DdType > const &  manager,
storm::expressions::Variable const &  blockVariable,
std::set< storm::expressions::Variable > const &  stateRowVariables,
std::set< storm::expressions::Variable > const &  stateColumnVariables,
bool  shiftStateVariables,
std::set< storm::expressions::Variable > const &  nondeterminismVariables = std::set<storm::expressions::Variable>() 
)

Definition at line 13 of file SignatureRefiner.cpp.

Member Function Documentation

◆ refine()

template<storm::dd::DdType DdType, typename ValueType >
Partition< DdType, ValueType > storm::dd::bisimulation::SignatureRefiner< DdType, ValueType >::refine ( Partition< DdType, ValueType > const &  oldPartition,
Signature< DdType, ValueType > const &  signature 
)

Definition at line 36 of file SignatureRefiner.cpp.


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