public final class DefaultPathEncoding extends PathEncoding
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 |
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.
|
getDefaultEncoding, getEncoding, getPathNodeType, getSourcePathNodeType
getBit, getCurrentStateDomain, getInnerInterface, getInterfaceBit, getInterfaceEncodingBDD, getInterfaceLength, getInterfaceSize, getInterfaceSizeIsGreaterOrEqual, getInterfaceSizeIsLessOrEqual, getInterfaceSizeType, getLength, getMaximumInterface, getOuterInterface, getStateBit, getStateEncodingBDD, getStateLength, getStateType, getSuccessorStateDomain, one, toString, zero
public RavenBDD getPathBit(BDDEncoding.StateType type, int source, int target)
PathEncoding
from
-th node
in the interface to the to
-th node of the interface.getPathBit
in class PathEncoding
type
- the state type, either current state or successor statesource
- the position of the interface nodetarget
- the index of the bit in the path encodingpublic RavenBDD getSourcePathBit(BDDEncoding.StateType type, int node)
PathEncoding
node
-th interface node is connected to at
least one of the source nodes.getSourcePathBit
in class PathEncoding
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)
PathEncoding
type
domain
of the BDDexistsPathBit
in class PathEncoding
type
- 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 interfacepublic String getBitType(int pos)
BDDEncoding
pos
.getBitType
in class BDDEncoding
pos
- the position of the bitpublic String printStates(RavenBDD stateSet)
BDDEncoding
printStates
in class BDDEncoding
stateSet
- the state set to be printed