storm::dd::bisimulation Namespace Reference

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

Enumerations
enum class	InitialPartitionMode { Regular , Finer }
enum class	QuotientFormat { Sparse , Dd }
enum class	RefinementMode { Full , ChangedStates }
enum class	ReuseMode { None , BlockNumbers }
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

InitialPartitionMode

enum class storm::dd::bisimulation::InitialPartitionMode

strong

Enumerator
Regular
Finer

Definition at line 7 of file InitialPartitionMode.h.

QuotientFormat

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

strong

Enumerator
Sparse
Dd

Definition at line 6 of file QuotientFormat.h.

RefinementMode

enum class storm::dd::bisimulation::RefinementMode

strong

Enumerator
Full
ChangedStates

Definition at line 7 of file RefinementMode.h.

ReuseMode

enum class storm::dd::bisimulation::ReuseMode

strong

Enumerator
None
BlockNumbers

Definition at line 7 of file ReuseMode.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 332 of file Partition.cpp.