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
static uint64_t	sylvan_hash (uint64_t a, uint64_t b)
	VOID_TASK_3 (sylvan_rehash, size_t, first, size_t, count, InternalSylvanSignatureRefinerBase *, refiner)
	The code below was taken from the SigrefMC implementation by Tom van Dijk, available at.
	VOID_TASK_1 (sylvan_grow_it, InternalSylvanSignatureRefinerBase *, refiner)
	VOID_TASK_1 (sylvan_grow, InternalSylvanSignatureRefinerBase *, refiner)
static uint64_t	sylvan_search_or_insert (uint64_t sig, uint64_t previous_block, InternalSylvanSignatureRefinerBase *refiner)
	TASK_1 (uint64_t, sylvan_decode_block, BDD, block)
	TASK_3 (BDD, sylvan_encode_block, BDD, vars, uint64_t, numberOfVariables, uint64_t, blockIndex)
	TASK_3 (BDD, sylvan_assign_block, BDD, sig, BDD, previous_block, InternalSylvanSignatureRefinerBase *, refiner)
	TASK_5 (BDD, sylvan_refine_partition, BDD, dd, BDD, previous_partition, BDD, nondetvars, BDD, vars, InternalSylvanSignatureRefinerBase *, refiner)
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)

Variables
static const uint64_t	NO_ELEMENT_MARKER = -1ull

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.

sylvan_hash()

static uint64_t storm::dd::bisimulation::sylvan_hash ( uint64_t  a, uint64_t  b  )

static

Definition at line 102 of file InternalSylvanSignatureRefiner.cpp.

sylvan_search_or_insert()

static uint64_t storm::dd::bisimulation::sylvan_search_or_insert ( uint64_t  sig, uint64_t  previous_block, InternalSylvanSignatureRefinerBase *  refiner  )

static

Definition at line 188 of file InternalSylvanSignatureRefiner.cpp.

TASK_1()

storm::dd::bisimulation::TASK_1	(	uint64_t	,
		sylvan_decode_block	,
		BDD	,
		block
	)

Definition at line 222 of file InternalSylvanSignatureRefiner.cpp.

TASK_3() [1/2]

storm::dd::bisimulation::TASK_3	(	BDD	,
		sylvan_assign_block	,
		BDD	,
		sig	,
		BDD	,
		previous_block	,
		InternalSylvanSignatureRefinerBase *	,
		refiner
	)

Definition at line 247 of file InternalSylvanSignatureRefiner.cpp.

TASK_3() [2/2]

storm::dd::bisimulation::TASK_3	(	BDD	,
		sylvan_encode_block	,
		BDD	,
		vars	,
		uint64_t	,
		numberOfVariables	,
		uint64_t	,
		blockIndex
	)

Definition at line 238 of file InternalSylvanSignatureRefiner.cpp.

TASK_5()

storm::dd::bisimulation::TASK_5	(	BDD	,
		sylvan_refine_partition	,
		BDD	,
		dd	,
		BDD	,
		previous_partition	,
		BDD	,
		nondetvars	,
		BDD	,
		vars	,
		InternalSylvanSignatureRefinerBase *	,
		refiner
	)

Definition at line 284 of file InternalSylvanSignatureRefiner.cpp.

VOID_TASK_1() [1/2]

storm::dd::bisimulation::VOID_TASK_1	(	sylvan_grow	,
		InternalSylvanSignatureRefinerBase *	,
		refiner
	)

Definition at line 176 of file InternalSylvanSignatureRefiner.cpp.

VOID_TASK_1() [2/2]

storm::dd::bisimulation::VOID_TASK_1	(	sylvan_grow_it	,
		InternalSylvanSignatureRefinerBase *	,
		refiner
	)

Definition at line 164 of file InternalSylvanSignatureRefiner.cpp.

VOID_TASK_3()

storm::dd::bisimulation::VOID_TASK_3	(	sylvan_rehash	,
		size_t	,
		first	,
		size_t	,
		count	,
		InternalSylvanSignatureRefinerBase *	,
		refiner
	)

The code below was taken from the SigrefMC implementation by Tom van Dijk, available at.

https://github.com/utwente-fmt/sigrefmc/

It provides a fully multi-threaded version of signature-based partition refinement and includes, amongst other things, a small custom-tailored hashmap that supports multi-threaded insertion.

The code was modified in minor places to account for necessary changes, for example to handle nondeterminism variables.

Definition at line 128 of file InternalSylvanSignatureRefiner.cpp.

Variable Documentation

NO_ELEMENT_MARKER

const uint64_t storm::dd::bisimulation::NO_ELEMENT_MARKER = -1ull

static

Definition at line 18 of file InternalSylvanSignatureRefiner.cpp.