storm::dd::bisimulation Namespace Reference

Classes
class	InternalRepresentativeComputer
class	InternalRepresentativeComputer< storm::dd::DdType::CUDD >
class	InternalRepresentativeComputer< storm::dd::DdType::Sylvan >
class	InternalRepresentativeComputerBase
class	InternalSignatureRefiner
class	InternalSignatureRefiner< storm::dd::DdType::CUDD, ValueType >
class	InternalSignatureRefiner< storm::dd::DdType::Sylvan, ValueType >
struct	InternalSignatureRefinerOptions
class	InternalSparseQuotientExtractor
class	InternalSparseQuotientExtractor< storm::dd::DdType::CUDD, ValueType >
class	InternalSparseQuotientExtractor< storm::dd::DdType::Sylvan, ValueType, ExportValueType >
class	InternalSparseQuotientExtractorBase
class	InternalSylvanSignatureRefinerBase
class	NondeterministicModelPartitionRefiner
class	PartialQuotientExtractor
class	Partition
class	PartitionRefiner
class	PreservationInformation
class	QuotientExtractor
class	ReuseWrapper
class	Signature
class	SignatureComputer
class	SignatureIterator
class	SignatureRefiner

Enumerations
enum class	QuotientFormat { Sparse , Dd }
enum class	SignatureMode { Eager , Lazy , Qualitative }
enum class	Status { Initialized , InComputation , FixedPoint }

Functions
template<storm::dd::DdType DdType>
void	enumerateBlocksRec (std::vector< storm::dd::Bdd< DdType > > const &stateSets, storm::dd::Bdd< DdType > const &currentStateSet, uint64_t offset, storm::expressions::Variable const &blockVariable, std::function< void(storm::dd::Bdd< DdType > const &)> const &callback)

Enumeration Type Documentation

QuotientFormat

enum class storm::dd::bisimulation::QuotientFormat

strong

Enumerator
Sparse
Dd

Definition at line 6 of file QuotientFormat.h.

SignatureMode

enum class storm::dd::bisimulation::SignatureMode

strong

Enumerator
Eager
Lazy
Qualitative

Definition at line 7 of file SignatureMode.h.

Status

enum class storm::dd::bisimulation::Status

strong

Enumerator
Initialized
InComputation
FixedPoint

Definition at line 7 of file Status.h.

Function Documentation

enumerateBlocksRec()

template<storm::dd::DdType DdType>

void storm::dd::bisimulation::enumerateBlocksRec	(	std::vector< storm::dd::Bdd< DdType > > const &	stateSets,
		storm::dd::Bdd< DdType > const &	currentStateSet,
		uint64_t	offset,
		storm::expressions::Variable const &	blockVariable,
		std::function< void(storm::dd::Bdd< DdType > const &)> const &	callback
	)

Definition at line 346 of file Partition.cpp.