public class AnotherPathEncoding extends PathEncoding
PathAutomaton
BDDEncoding.StateType
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 |
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.
|
existsPathBit, 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 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