de.uni_due.inf.ti.raven.encodings

Class DefaultPathEncoding

java.lang.Object

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

de.uni_due.inf.ti.raven.encodings.PathEncoding

de.uni_due.inf.ti.raven.encodings.DefaultPathEncoding

public final class DefaultPathEncoding
extends PathEncoding

This class provides a concrete implementation of an encoding for path automata. The state encoding is as follows: b₁ ... b_l (m_0,0 ... m_n-1,0) ... (m_0,n-1 ... m_n-1,n-1), where l = log₂(n) is the binary logarithm of the maximum interface size n. The block b₁ ... b_l encodes the interface size to which the current state belongs, the block m_0,i ... m_n-1,i the adjacency bits of the i-th interface node in the current state.

Version:

$Revision: 1.16 $

Author:

Christoph Blume, Dennis Nolte

See Also:

PathAutomaton

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
RavenBDD	existsPathBit(BDDEncoding.StateType type, RavenBDD bdd, int source, int target) Returns the BDD which describes the existence of an adjacency bit in the type domain of the BDD
String	getBitType(int pos) Returns a string indicating which information is encoded by bit of the given position pos.
RavenBDD	getPathBit(BDDEncoding.StateType type, int source, int target) Returns a BDD which encodes the (non)-existence of a path from the from-th node in the interface to the to-th node of the interface.
RavenBDD	getSourcePathBit(BDDEncoding.StateType type, int node) Returns the BDD which encodes whether the node-th interface node is connected to at least one of the source nodes.
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.PathEncoding

getDefaultEncoding, getEncoding, getPathNodeType, getSourcePathNodeType

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

getPathBit

public RavenBDD getPathBit(BDDEncoding.StateType type,
                  int source,
                  int target)

Description copied from class: PathEncoding

Returns a BDD which encodes the (non)-existence of a path from the from-th node in the interface to the to-th node of the interface.

Specified by:

getPathBit in class PathEncoding

Parameters:

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

source - the position of the interface node

target - the index of the bit in the path encoding

Returns:

the BDD node representing the bit of the path encoding

getSourcePathBit

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

Description copied from class: PathEncoding

Returns the BDD which encodes whether the node-th interface node is connected to at least one of the source nodes.

Specified by:

getSourcePathBit in class PathEncoding

Parameters:

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

node - the index of the node in the path encoding

Returns:

the BDD node representing the connection bit of the path encoding

existsPathBit

public RavenBDD existsPathBit(BDDEncoding.StateType type,
                     RavenBDD bdd,
                     int source,
                     int target)

Description copied from class: PathEncoding

Returns the BDD which describes the existence of an adjacency bit in the type domain of the BDD

Overrides:

existsPathBit in class PathEncoding

Parameters:

type - the StateType where the adjacency bit is extracted

bdd - the BDD which is observed

source - the position of the source not in the interface

target - the position of the target not in the interface

Returns:

the BDD representing the existence of the bit in the path encoding

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

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