Package | Description |
---|---|
de.uni_due.inf.ti.raven.encodings |
Classes to encode the state space and the transitions of the various graph automata.
|
Modifier and Type | Method and Description |
---|---|
static BDDEncoding.StateType |
BDDEncoding.StateType.valueOf(String name)
Returns the enum constant of this type with the specified name.
|
static BDDEncoding.StateType[] |
BDDEncoding.StateType.values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
Modifier and Type | Method and Description |
---|---|
RavenBDD |
DefaultPathEncoding.existsPathBit(BDDEncoding.StateType type,
RavenBDD bdd,
int source,
int target) |
RavenBDD |
PathEncoding.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 |
abstract RavenBDD |
ColorabilityEncoding.getBDDForColor(BDDEncoding.StateType type,
int node,
int color)
Constructs a BDD which is
true if and only if in the state state
the node -th interface node either has some color color . |
RavenBDD |
DefaultColorabilityEncoding.getBDDForColor(BDDEncoding.StateType type,
int node,
int color) |
RavenBDD |
BDDEncoding.getBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes in state
state the pos -th bit the encoding. |
abstract RavenBDD |
ColorabilityEncoding.getColorBit(BDDEncoding.StateType type,
int node,
int bit)
Returns the
bit -th BDD node of the color encoding of the node -th node
for the state state . |
RavenBDD |
DefaultColorabilityEncoding.getColorBit(BDDEncoding.StateType type,
int node,
int bit) |
abstract RavenBDD |
LinkEncoding.getConnectedNodeBit(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes in state
state whether the pos -th node of the
interface is connected to an initial node or not. |
RavenBDD |
AnotherLinkEncoding.getConnectedNodeBit(BDDEncoding.StateType type,
int node)
Get the connected (i.e. 2nd) bit of the
node -th (starting with 0) node markings. |
RavenBDD |
DefaultLinkEncoding.getConnectedNodeBit(BDDEncoding.StateType type,
int node)
Get the connected (i.e. 2nd) bit of the
node -th (starting with 0) node markings. |
abstract RavenBDD |
DominatingSetEncoding.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 |
DefaultDominatingSetEncoding.getDominationBit(BDDEncoding.StateType type,
int node) |
RavenBDD |
AnotherDominatingSetEncoding.getDominationBit(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
DominatingSetEncoding.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 |
DefaultDominatingSetEncoding.getDominationSizeBit(BDDEncoding.StateType type,
int pos) |
RavenBDD |
AnotherDominatingSetEncoding.getDominationSizeBit(BDDEncoding.StateType type,
int pos) |
abstract RavenBDD |
SubgraphEncoding.getEdgeBit(BDDEncoding.StateType type,
int edge)
Returns a BDD which encodes that in state
state the edge -th subgraph edge
has been recognized if and only if the BDD is true . |
RavenBDD |
DefaultSubgraphEncoding.getEdgeBit(BDDEncoding.StateType type,
int edge) |
abstract RavenBDD |
NoIsolatedNodesEncoding.getHasIsolatedNodes(BDDEncoding.StateType type)
Returns a BDD which encodes that in state
state isolated nodes are present
if and only if the BDD is true . |
RavenBDD |
DefaultNoIsolatedNodesEncoding.getHasIsolatedNodes(BDDEncoding.StateType type) |
abstract RavenBDD |
LinkEncoding.getInitialNodeBit(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes in state
state whether the pos -th node of the
interface is an initial node or not. |
RavenBDD |
AnotherLinkEncoding.getInitialNodeBit(BDDEncoding.StateType type,
int node)
Get the initial (i.e. 1st) bit of the
node -th (starting with 0) node markings. |
RavenBDD |
DefaultLinkEncoding.getInitialNodeBit(BDDEncoding.StateType type,
int node)
Get the initial (i.e. 1st) bit of the
node -th (starting with 0) node markings. |
RavenBDD |
BDDEncoding.getInterfaceBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes the
pos -th interface bit for
the state type type . |
RavenBDD |
BDDEncoding.getInterfaceSize(BDDEncoding.StateType type,
int size)
Returns a BDD which encodes the interface size
size for
the state state . |
RavenBDD |
BDDEncoding.getInterfaceSizeIsGreaterOrEqual(BDDEncoding.StateType type,
int size)
Returns a BDD encoding that in the state type
type the size of the
interface is greater or equal to size if and only if the BDD is true . |
RavenBDD |
BDDEncoding.getInterfaceSizeIsLessOrEqual(BDDEncoding.StateType type,
int size)
Returns a BDD encoding that in the state
state the size of the
interface is less or equal to size if and only if the BDD is true . |
abstract RavenBDD |
NoIsolatedNodesEncoding.getIsNodeIsolated(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that in state
state the node -th interface node
is isolated if and only if the BDD is true . |
RavenBDD |
DefaultNoIsolatedNodesEncoding.getIsNodeIsolated(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
SubgraphEncoding.getMappingBit(BDDEncoding.StateType type,
int node,
int pos)
Returns a BDD which encodes that in state
state the node -th subgraph node
is the image of pos -th interface node (of the function mapping the interface into
the subgraph node set) if and only if the BDD is true . |
RavenBDD |
DefaultSubgraphEncoding.getMappingBit(BDDEncoding.StateType type,
int node,
int size) |
abstract RavenBDD |
DominatingSetEncoding.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 |
DefaultVertexCoverEncoding.getMembershipBit(BDDEncoding.StateType type,
int node) |
RavenBDD |
DefaultDominatingSetEncoding.getMembershipBit(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
VertexCoverEncoding.getMembershipBit(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that the
node -th node of the interface
is a member of the vertex cover. |
RavenBDD |
AnotherDominatingSetEncoding.getMembershipBit(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
SubgraphEncoding.getNodeBit(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that in state
state the node -th subgraph node
has been recognized if and only if the BDD is true . |
RavenBDD |
DefaultSubgraphEncoding.getNodeBit(BDDEncoding.StateType type,
int node) |
RavenBDD |
AnotherPathEncoding.getPathBit(BDDEncoding.StateType type,
int source,
int target) |
RavenBDD |
DefaultPathEncoding.getPathBit(BDDEncoding.StateType type,
int source,
int target) |
abstract RavenBDD |
PathEncoding.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. |
RavenBDD |
DefaultEdgeCountingEncoding.getRemainderBit(BDDEncoding.StateType type,
int pos) |
abstract RavenBDD |
CountingEncoding.getRemainderBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes in state
state the pos -th bit of the
remainder. |
RavenBDD |
DefaultVertexCountingEncoding.getRemainderBit(BDDEncoding.StateType type,
int pos) |
RavenBDD |
UnionEncoding.getSeparationBit(BDDEncoding.StateType type)
Returns a BDD which encodes that in state
state the separation bit has been set if
and only if the BDD is true . |
RavenBDD |
AnotherPathEncoding.getSourcePathBit(BDDEncoding.StateType type,
int node) |
RavenBDD |
DefaultPathEncoding.getSourcePathBit(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
PathEncoding.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. |
RavenBDD |
BDDEncoding.getStateBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes the
pos -th state bit for
the state type type . |
abstract RavenBDD |
DominatingSetEncoding.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 . |
RavenBDD |
DefaultVertexCoverEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node) |
RavenBDD |
DefaultDominatingSetEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
NoIsolatedNodesEncoding.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 . |
abstract RavenBDD |
VertexCoverEncoding.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 . |
RavenBDD |
AnotherDominatingSetEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node) |
RavenBDD |
DefaultNoIsolatedNodesEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node) |
RavenBDD |
DefaultMinimumBoundEncoding.getValueBit(BDDEncoding.StateType type,
int pos) |
RavenBDD |
DefaultMaximumBoundEncoding.getValueBit(BDDEncoding.StateType type,
int pos) |
abstract RavenBDD |
BoundEncoding.getValueBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes the
pos -th bit of the value of the node/edge counter. |
RavenBDD |
DefaultVertexCoverEncoding.getVertexCoverSizeBit(BDDEncoding.StateType type,
int pos) |
abstract RavenBDD |
VertexCoverEncoding.getVertexCoverSizeBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes in state
state the pos -th bit of the
current size of the vertex cover. |