de.uni_due.inf.ti.raven.encodings

Class AnotherDominatingSetEncoding

java.lang.Object

de.uni_due.inf.ti.raven.encodings.BDDEncoding

de.uni_due.inf.ti.raven.encodings.DominatingSetEncoding

de.uni_due.inf.ti.raven.encodings.AnotherDominatingSetEncoding

public class AnotherDominatingSetEncoding
extends DominatingSetEncoding

This class provides a concrete implementation of an encoding for dominating set automata. The state encoding is as follows: b₁ ... b_l m₁ ... m_k d₁ ... d_k s₁ ... s_t, where k is the maximum interface size, l = log₂(k) is the binary logarithm of k and t is the is the binary logarithm of the maximum dominating set size. The block b₁ ... b_l encodes the interface size to which the current state belongs, the block m₁ ... m_k encodes which nodes, currently in the interface, belong to the dominating set, the block d₁ ... d_k encodes which nodes, currently in the interface, are dominated by some node and the block s₁ ... s_t encodes the size of the dominating set in the current state.

Version:

$Revision: 1.19 $

Author:

Christoph Blume

See Also:

DominatingSetAutomaton

Nested Class Summary

Nested classes/interfaces inherited from class de.uni_due.inf.ti.raven.encodings.BDDEncoding

BDDEncoding.StateType

Method Summary

Methods

Modifier and Type	Method and Description
String	getBitType(int pos) Returns a string indicating which information is encoded by bit of the given position pos.
RavenBDD	getDominationBit(BDDEncoding.StateType type, int node) Returns a BDD which encodes that in state state the node-th interface node is dominated by some node of the dominating set if and only if the BDD is true.
RavenBDD	getDominationSizeBit(BDDEncoding.StateType type, int pos) Returns a BDD which encodes in state state the pos-th bit of the current size of the dominating set.
RavenBDD	getMembershipBit(BDDEncoding.StateType type, int node) Returns a BDD which encodes that the node-th node of the interface is a member of the dominating set.
RavenBDD	getUndefinedNode(BDDEncoding.StateType type, int node) Returns a BDD which encodes that in state state the node-th interface node is not defined if and only if the BDD is true.
String	printStates(RavenBDD stateSet) Prints a single state (seen as singleton state set) or a set of states.

Methods inherited from class de.uni_due.inf.ti.raven.encodings.DominatingSetEncoding

getDefaultEncoding, getDominationBitLength, getDominationNodeType, getDominationNumber, getDominationSetSizeType, getEncoding, getMembershipNodeType

Methods inherited from class de.uni_due.inf.ti.raven.encodings.BDDEncoding

getBit, getCurrentStateDomain, getInnerInterface, getInterfaceBit, getInterfaceEncodingBDD, getInterfaceLength, getInterfaceSize, getInterfaceSizeIsGreaterOrEqual, getInterfaceSizeIsLessOrEqual, getInterfaceSizeType, getLength, getMaximumInterface, getOuterInterface, getStateBit, getStateEncodingBDD, getStateLength, getStateType, getSuccessorStateDomain, one, toString, zero

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Method Detail

getBitType

public String getBitType(int pos)

Description copied from class: BDDEncoding

Returns a string indicating which information is encoded by bit of the given position pos.

Specified by:

getBitType in class BDDEncoding

Parameters:

pos - the position of the bit

Returns:

the type of information encoded by the specified bit

getMembershipBit

public RavenBDD getMembershipBit(BDDEncoding.StateType type,
                        int node)

Description copied from class: DominatingSetEncoding

Returns a BDD which encodes that the node-th node of the interface is a member of the dominating set.

Specified by:

getMembershipBit in class DominatingSetEncoding

Parameters:

type - the state type, either current state or successor state

node - the index of the interface node

Returns:

a BDD encoding the membership of the node

getDominationBit

public RavenBDD getDominationBit(BDDEncoding.StateType type,
                        int node)

Description copied from class: DominatingSetEncoding

Returns a BDD which encodes that in state state the node-th interface node is dominated by some node of the dominating set if and only if the BDD is true.

Specified by:

getDominationBit in class DominatingSetEncoding

Parameters:

type - the state type, either current state or successor state

node - the position of the interface node

Returns:

a BDD encoding that the interface node is dominated

getUndefinedNode

public RavenBDD getUndefinedNode(BDDEncoding.StateType type,
                        int node)

Description copied from class: DominatingSetEncoding

Returns a BDD which encodes that in state state the node-th interface node is not defined if and only if the BDD is true.

Specified by:

getUndefinedNode in class DominatingSetEncoding

Parameters:

type - the state type, either current state or successor state

node - the position of the interface node

Returns:

a BDD encoding that the interface node is not defined

getDominationSizeBit

public RavenBDD getDominationSizeBit(BDDEncoding.StateType type,
                            int pos)

Description copied from class: DominatingSetEncoding

Returns a BDD which encodes in state state the pos-th bit of the current size of the dominating set.

Specified by:

getDominationSizeBit in class DominatingSetEncoding

Parameters:

type - the state type, either current state or successor state

pos - the position of the bit

Returns:

a BDD encoding a bit of the dominating set size

printStates

public String printStates(RavenBDD stateSet)

Description copied from class: BDDEncoding

Prints a single state (seen as singleton state set) or a set of states.

Specified by:

printStates in class BDDEncoding

Parameters:

stateSet - the state set to be printed

Returns:

the string representation of the state set