public abstract class PathEncoding extends BDDEncoding
Note: The concrete implementation of a path encoding can be found in classes extending this abstract class.
DefaultPathEncoding
,
PathAutomaton
BDDEncoding.StateType
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 |
static PathEncoding |
getDefaultEncoding(int maximumInterface,
int innerInterface,
int outerInterface)
Returns the default BDD encoding for a path instance with a
maximum interface size of
maximumInterface . |
static PathEncoding |
getEncoding(int maximumInterface,
int innerInterface,
int outerInterface,
String encodingName)
Returns the BDD encoding for a path instance given by the class name
name with a
maximum interface size of maximumInterface and a number of colors of colors . |
abstract RavenBDD |
getPathBit(BDDEncoding.StateType type,
int from,
int to)
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. |
static String |
getPathNodeType(int from,
int to)
Returns the type string indicating the (non-)existence of a path from the
from -th
interface node to the to -th interface node. |
abstract 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. |
static String |
getSourcePathNodeType(int node)
Returns the type string indicating the (non-)existence of a path from a source node to
the
node -th interface node. |
getBit, getBitType, getCurrentStateDomain, getInnerInterface, getInterfaceBit, getInterfaceEncodingBDD, getInterfaceLength, getInterfaceSize, getInterfaceSizeIsGreaterOrEqual, getInterfaceSizeIsLessOrEqual, getInterfaceSizeType, getLength, getMaximumInterface, getOuterInterface, getStateBit, getStateEncodingBDD, getStateLength, getStateType, getSuccessorStateDomain, one, printStates, toString, zero
public static final PathEncoding getDefaultEncoding(int maximumInterface, int innerInterface, int outerInterface)
maximumInterface
.maximumInterface
- the maximum interface sizeinnerInterface
- size of the inner interfaceouterInterface
- size of the outer interfacepublic static final PathEncoding getEncoding(int maximumInterface, int innerInterface, int outerInterface, String encodingName)
name
with a
maximum interface size of maximumInterface
and a number of colors of colors
.
If no path encoding with the given name can be found the default encoding is returned.maximumInterface
- the maximum interface sizeinnerInterface
- size of the inner interfaceouterInterface
- size of the outer interfaceencodingName
- the class name of the dominating set encoding classpublic static final String getPathNodeType(int from, int to)
from
-th
interface node to the to
-th interface node.from
- the position of the source nodeto
- the position of the target nodepublic static final String getSourcePathNodeType(int node)
node
-th interface node.node
- the position of the node (in the interface)public abstract RavenBDD getPathBit(BDDEncoding.StateType type, int from, int to)
from
-th node
in the interface to the to
-th node of the interface.type
- the state type, either current state or successor statefrom
- the position of the interface nodeto
- the index of the bit in the path encodingpublic abstract RavenBDD getSourcePathBit(BDDEncoding.StateType type, int node)
node
-th interface node is connected to at
least one of the source nodes.type
- the state type, either current state or successor statenode
- the index of the node in the path encodingpublic RavenBDD existsPathBit(BDDEncoding.StateType type, RavenBDD bdd, int source, int target)
type
domain
of the BDDtype
- the StateType where the adjacency bit is extractedbdd
- the BDD which is observedsource
- the position of the source not in the interfacetarget
- the position of the target not in the interface