storm::dd::Odd Class Reference

#include <Odd.h>

Public Member Functions
	Odd (std::shared_ptr< Odd > elseNode, uint_fast64_t elseOffset, std::shared_ptr< Odd > thenNode, uint_fast64_t thenOffset)
	Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor.
	Odd ()=default
	Odd (Odd const &other)=default
Odd &	operator= (Odd const &other)=default
	Odd (Odd &&other)=default
Odd &	operator= (Odd &&other)=default
Odd const &	getThenSuccessor () const
	Retrieves the then-successor of this ODD node.
Odd const &	getElseSuccessor () const
	Retrieves the else-successor of this ODD node.
uint_fast64_t	getElseOffset () const
	Retrieves the else-offset of this ODD node.
void	setElseOffset (uint_fast64_t newOffset)
	Sets the else-offset of this ODD node.
uint_fast64_t	getThenOffset () const
	Retrieves the then-offset of this ODD node.
void	setThenOffset (uint_fast64_t newOffset)
	Sets the then-offset of this ODD node.
uint_fast64_t	getTotalOffset () const
	Retrieves the total offset, i.e., the sum of the then- and else-offset.
uint_fast64_t	getNodeCount () const
	Retrieves the size of the ODD.
uint_fast64_t	getHeight () const
	Retrieves the height of the ODD.
bool	isTerminalNode () const
	Checks whether the given ODD node is a terminal node, i.e.
template<typename ValueType >
void	expandExplicitVector (storm::dd::Odd const &newOdd, std::vector< ValueType > const &oldValues, std::vector< ValueType > &newValues) const
	Adds the old values to the new values.
void	oldToNewIndex (storm::dd::Odd const &newOdd, std::function< void(uint64_t oldOffset, uint64_t newOffset)> const &callback) const
	Translates the indices of the old ODD to that of the new ODD by calling the callback for each old-new offset pair.
void	exportToDot (std::string const &filename) const
	Exports the ODD in the dot format to the given file.
void	exportToText (std::string const &filename) const
	Exports the ODD in the text format to the given file.
storm::storage::BitVector	getEncoding (uint64_t offset, uint64_t variableCount=0) const
	Retrieves the encoding for the given offset.

Detailed Description

Definition at line 16 of file Odd.h.

Constructor & Destructor Documentation

Odd() [1/4]

storm::dd::Odd::Odd	(	std::shared_ptr< Odd >	elseNode,
		uint_fast64_t	elseOffset,
		std::shared_ptr< Odd >	thenNode,
		uint_fast64_t	thenOffset
	)

Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor.

Parameters

dd	The DD node associated with this ODD node.
elseNode	The else-successor of thie ODD node.
elseOffset	The offset of the else-successor.
thenNode	The then-successor of thie ODD node.
thenOffset	The offset of the then-successor.

Definition at line 18 of file Odd.cpp.

Odd() [2/4]

storm::dd::Odd::Odd ( )

default

Odd() [3/4]

storm::dd::Odd::Odd ( Odd const &  other )

default

Odd() [4/4]

storm::dd::Odd::Odd ( Odd &&  other )

default

Member Function Documentation

expandExplicitVector()

template<typename ValueType >

template void storm::dd::Odd::expandExplicitVector	(	storm::dd::Odd const &	newOdd,
		std::vector< ValueType > const &	oldValues,
		std::vector< ValueType > &	newValues
	)		const

Adds the old values to the new values.

It does so by writing the old values at their correct positions wrt. to the new ODD.

Parameters

newOdd	The new ODD to use.
oldValues	The old vector of values (which is being read).
newValues	The new vector of values (which is being written).

Definition at line 79 of file Odd.cpp.

exportToDot()

void storm::dd::Odd::exportToDot

(

std::string const &

filename

)

const

Exports the ODD in the dot format to the given file.

Parameters

filename

The name of the file to which to write the dot output.

Definition at line 127 of file Odd.cpp.

exportToText()

void storm::dd::Odd::exportToText

(

std::string const &

filename

)

const

Exports the ODD in the text format to the given file.

Parameters

filename

The name of the file to which to write the dot output.

Definition at line 172 of file Odd.cpp.

getElseOffset()

uint_fast64_t storm::dd::Odd::getElseOffset

(

)

const

Retrieves the else-offset of this ODD node.

Returns

The else-offset of this ODD node.

Definition at line 31 of file Odd.cpp.

getElseSuccessor()

Odd const & storm::dd::Odd::getElseSuccessor

(

)

const

Retrieves the else-successor of this ODD node.

Returns

The else-successor of this ODD node.

Definition at line 27 of file Odd.cpp.

getEncoding()

storm::storage::BitVector storm::dd::Odd::getEncoding	(	uint64_t	offset,
		uint64_t	variableCount = 0
	)		const

Retrieves the encoding for the given offset.

Parameters

offset	The target offset.
variableCount	If not null, this indicates how many variables are contained in the encoding. If 0, this number is automatically determined.

Definition at line 190 of file Odd.cpp.

getHeight()

uint_fast64_t storm::dd::Odd::getHeight

(

)

const

Retrieves the height of the ODD.

Returns

The height of the ODD.

Definition at line 65 of file Odd.cpp.

getNodeCount()

uint_fast64_t storm::dd::Odd::getNodeCount

(

)

const

Retrieves the size of the ODD.

Note: the size is computed by a traversal, so this may be costlier than expected.

Returns

The size (in nodes) of this ODD.

Definition at line 51 of file Odd.cpp.

getThenOffset()

uint_fast64_t storm::dd::Odd::getThenOffset

(

)

const

Retrieves the then-offset of this ODD node.

Returns

The then-offset of this ODD node.

Definition at line 39 of file Odd.cpp.

getThenSuccessor()

Odd const & storm::dd::Odd::getThenSuccessor

(

)

const

Retrieves the then-successor of this ODD node.

Returns

The then-successor of this ODD node.

Definition at line 23 of file Odd.cpp.

getTotalOffset()

uint_fast64_t storm::dd::Odd::getTotalOffset

(

)

const

Retrieves the total offset, i.e., the sum of the then- and else-offset.

Returns

The total offset of this ODD.

Definition at line 47 of file Odd.cpp.

isTerminalNode()

bool storm::dd::Odd::isTerminalNode

(

)

const

Checks whether the given ODD node is a terminal node, i.e.

has no successors.

Returns

True iff the node is terminal.

Definition at line 74 of file Odd.cpp.

oldToNewIndex()

void storm::dd::Odd::oldToNewIndex	(	storm::dd::Odd const &	newOdd,
		std::function< void(uint64_t oldOffset, uint64_t newOffset)> const &	callback
	)		const

Translates the indices of the old ODD to that of the new ODD by calling the callback for each old-new offset pair.

Note that for each old offset, there may be multiple new offsets. The new ODD is expected to extend the old ODD by adding layers at the bottom.

Parameters

newOdd	The new ODD to use.
callback	The callback function.

Definition at line 98 of file Odd.cpp.

operator=() [1/2]

Odd & storm::dd::Odd::operator= ( Odd &&  other )

default

operator=() [2/2]

Odd & storm::dd::Odd::operator= ( Odd const &  other )

default

setElseOffset()

void storm::dd::Odd::setElseOffset

(

uint_fast64_t

newOffset

)

Sets the else-offset of this ODD node.

Parameters

newOffset

The new else-offset of this ODD node.

Definition at line 35 of file Odd.cpp.

setThenOffset()

void storm::dd::Odd::setThenOffset

(

uint_fast64_t

newOffset

)

Sets the then-offset of this ODD node.

Parameters

newOffset

The new then-offset of this ODD node.

Definition at line 43 of file Odd.cpp.

---

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

• src/storm/storage/dd/Odd.h
• src/storm/storage/dd/Odd.cpp