storm::dd Namespace Reference

Namespaces
namespace	bisimulation

Classes
class	Add
class	AddIterator
class	AddIterator< DdType::CUDD, ValueType >
class	AddIterator< DdType::Sylvan, ValueType >
class	Bdd
class	BisimulationDecomposition
struct	CuddPointerPairHash
class	Dd
class	DdManager
class	DdMetaVariable
struct	FromVectorHelper
struct	FromVectorHelper< LibraryType, storm::RationalFunction >
class	InternalAdd
class	InternalAdd< DdType::CUDD, ValueType >
class	InternalAdd< DdType::Sylvan, ValueType >
class	InternalBdd
class	InternalBdd< DdType::CUDD >
class	InternalBdd< DdType::Sylvan >
class	InternalDdManager
class	InternalDdManager< DdType::CUDD >
class	InternalDdManager< DdType::Sylvan >
class	Odd
struct	SylvanMTBDDPairHash
struct	SylvanMTBDDPairLess

Enumerations
enum class	MetaVariableType { Bool , Int , BitVector }
enum class	DdType { CUDD , Sylvan }
enum class	MetaVariablePosition { Above , Below }

Functions
bool	sylvan_bdd_matches_variable_index (BDD node, uint64_t variableIndex, int64_t offset=0)
	Retrieves whether the topmost variable in the BDD is the one with the given index.
bool	sylvan_mtbdd_matches_variable_index (MTBDD node, uint64_t variableIndex, int64_t offset=0)
	Retrieves whether the topmost variable in the MTBDD is the one with the given index.
template<DdType LibraryType, typename ValueType >
std::ostream &	operator<< (std::ostream &out, Add< LibraryType, ValueType > const &add)
template std::ostream &	operator<< (std::ostream &out, Add< storm::dd::DdType::CUDD, double > const &add)
template std::ostream &	operator<< (std::ostream &out, Add< storm::dd::DdType::Sylvan, double > const &add)
template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< PartitionRefiner< DdType, ValueType > >	createRefiner (storm::models::symbolic::Model< DdType, ValueType > const &model, Partition< DdType, ValueType > const &initialPartition)
void	getEncodingRec (Odd const &odd, uint64_t index, uint64_t offset, storm::storage::BitVector &result)
	VOID_TASK_0 (gc_start)
	VOID_TASK_0 (gc_end)
	VOID_TASK_2 (execute_sylvan, std::function< void()> const *, f, std::exception_ptr *, e)
uint_fast64_t	findLargestPowerOfTwoFitting (uint_fast64_t number)

Enumeration Type Documentation

DdType

enum class storm::dd::DdType

strong

Enumerator
CUDD
Sylvan

Definition at line 6 of file DdType.h.

MetaVariablePosition

enum class storm::dd::MetaVariablePosition

strong

Enumerator
Above
Below

Definition at line 10 of file MetaVariablePosition.h.

MetaVariableType

enum class storm::dd::MetaVariableType

strong

Enumerator
Bool
Int
BitVector

Definition at line 19 of file DdMetaVariable.h.

Function Documentation

createRefiner()

template<storm::dd::DdType DdType, typename ValueType >

std::unique_ptr< PartitionRefiner< DdType, ValueType > > storm::dd::createRefiner	(	storm::models::symbolic::Model< DdType, ValueType > const &	model,
		Partition< DdType, ValueType > const &	initialPartition
	)

Definition at line 26 of file BisimulationDecomposition.cpp.

findLargestPowerOfTwoFitting()

uint_fast64_t storm::dd::findLargestPowerOfTwoFitting

(

uint_fast64_t

number

)

Definition at line 57 of file InternalSylvanDdManager.cpp.

getEncodingRec()

void storm::dd::getEncodingRec	(	Odd const &	odd,
		uint64_t	index,
		uint64_t	offset,
		storm::storage::BitVector &	result
	)

Definition at line 176 of file Odd.cpp.

operator<<() [1/3]

template<DdType LibraryType, typename ValueType >

std::ostream & storm::dd::operator<<	(	std::ostream &	out,
		Add< LibraryType, ValueType > const &	add
	)

Definition at line 1166 of file Add.cpp.

operator<<() [2/3]

template std::ostream & storm::dd::operator<<	(	std::ostream &	out,
		Add< storm::dd::DdType::CUDD, double > const &	add
	)

operator<<() [3/3]

template std::ostream & storm::dd::operator<<	(	std::ostream &	out,
		Add< storm::dd::DdType::Sylvan, double > const &	add
	)

sylvan_bdd_matches_variable_index()

bool storm::dd::sylvan_bdd_matches_variable_index	(	BDD	node,
		uint64_t	variableIndex,
		int64_t	offset = 0
	)

Retrieves whether the topmost variable in the BDD is the one with the given index.

Parameters

node	The top node of the BDD.
variableIndex	The variable index.
offset	An offset that is applied to the index of the top variable in the BDD.

Returns

True iff the BDD's top variable has the given index.

Definition at line 6 of file sylvan.cpp.

sylvan_mtbdd_matches_variable_index()

bool storm::dd::sylvan_mtbdd_matches_variable_index	(	MTBDD	node,
		uint64_t	variableIndex,
		int64_t	offset = 0
	)

Retrieves whether the topmost variable in the MTBDD is the one with the given index.

Parameters

node	The top node of the BDD.
variableIndex	The variable index.
offset	An offset that is applied to the index of the top variable in the BDD.

Returns

True iff the BDD's top variable has the given index.

Definition at line 10 of file sylvan.cpp.

VOID_TASK_0() [1/2]

storm::dd::VOID_TASK_0

(

gc_end

)

Definition at line 33 of file InternalSylvanDdManager.cpp.

VOID_TASK_0() [2/2]

storm::dd::VOID_TASK_0

(

gc_start

)

Definition at line 29 of file InternalSylvanDdManager.cpp.

VOID_TASK_2()

storm::dd::VOID_TASK_2	(	execute_sylvan	,
		std::function< void()> const *	,
		f	,
		std::exception_ptr *	,
		e
	)

Definition at line 38 of file InternalSylvanDdManager.cpp.