public abstract class BDDEncoding extends Object
Automaton
Modifier and Type | Class and Description |
---|---|
static class |
BDDEncoding.StateType
Enumeration of state types to distinguish between bits used for different states
(e.g. in relations on the state set)
|
Modifier and Type | Method and Description |
---|---|
RavenBDD |
getBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes in state
state the pos -th bit the encoding. |
abstract String |
getBitType(int pos)
Returns a string indicating which information is encoded by bit of the given position
pos . |
RavenBDDDomain |
getCurrentStateDomain()
Returns the BDD domain for the (current) states
(of the transition relations)
|
int |
getInnerInterface()
Returns the inner interface size
|
RavenBDD |
getInterfaceBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes the
pos -th interface bit for
the state type type . |
RavenBDD |
getInterfaceEncodingBDD()
Returns a BDD encoding the bits of the interface
in the encoding for the current state.
|
int |
getInterfaceLength()
Returns the bit length of the interface encoding.
|
RavenBDD |
getInterfaceSize(BDDEncoding.StateType type,
int size)
Returns a BDD which encodes the interface size
size for
the state state . |
RavenBDD |
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 |
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 . |
static String |
getInterfaceSizeType()
Returns the type string indicating the bits for the interface size.
|
int |
getLength()
Returns the bit length of this BDD encoding
|
int |
getMaximumInterface()
Returns the maximum interface size.
|
int |
getOuterInterface()
Returns the outer interface size
|
RavenBDD |
getStateBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes the
pos -th state bit for
the state type type . |
RavenBDD |
getStateEncodingBDD()
Returns a BDD encoding the bits of the state information
in the encoding for the current state.
|
int |
getStateLength()
Returns the bit length of the state encoding.
|
static String |
getStateType()
Returns the type string indicating the bits for the state encoding.
|
RavenBDDDomain |
getSuccessorStateDomain()
Returns the BDD domain for the successor states
of the transition relations
|
RavenBDD |
one()
Returns the
One -BDD for this encoding. |
abstract String |
printStates(RavenBDD stateSet)
Prints a single state (seen as singleton state set) or a set of states.
|
String |
toString() |
RavenBDD |
zero()
Returns the
Zero -BDD for this encoding. |
public static final String getInterfaceSizeType()
public static final String getStateType()
public abstract String getBitType(int pos)
pos
.pos
- the position of the bitpublic abstract String printStates(RavenBDD stateSet)
stateSet
- the state set to be printedpublic final int getLength()
public final RavenBDD getBit(BDDEncoding.StateType type, int pos)
state
the pos
-th bit the encoding.type
- the state type, either current state or successor statepos
- the position of the bitpublic final int getMaximumInterface()
public final int getInnerInterface()
public final int getOuterInterface()
public final int getInterfaceLength()
getInterfaceBit(StateType, int)
public final int getStateLength()
getStateBit(StateType, int)
public final RavenBDD getInterfaceBit(BDDEncoding.StateType type, int pos)
pos
-th interface bit for
the state type type
.type
- the state type, either current state or successor statepos
- the index of the interface bitgetInterfaceLength()
public final RavenBDD getStateBit(BDDEncoding.StateType type, int pos)
pos
-th state bit for
the state type type
.type
- the state type, either current state or successor statepos
- the index of the interface bitpublic final RavenBDD getInterfaceSize(BDDEncoding.StateType type, int size)
size
for
the state state
.type
- the state type, either current state or successor statesize
- the size of the interfacegetInterfaceSizeIsGreaterOrEqual(StateType, int)
,
getInterfaceSizeIsLessOrEqual(StateType, int)
,
BDDEncoding.StateType
public final RavenBDD getInterfaceSizeIsLessOrEqual(BDDEncoding.StateType type, int size)
state
the size of the
interface is less or equal to size
if and only if the BDD is true
.type
- the state type, either current state or successor statesize
- the maximum size of the interfacesize
getInterfaceSizeIsGreaterOrEqual(StateType, int)
,
getInterfaceSize(StateType, int)
public final RavenBDD getInterfaceSizeIsGreaterOrEqual(BDDEncoding.StateType type, int size)
type
the size of the
interface is greater or equal to size
if and only if the BDD is true
.type
- the state type, either current state or successor statesize
- the minimum size of the interfacesize
getInterfaceSizeIsLessOrEqual(StateType, int)
,
getInterfaceSize(StateType, int)
public final RavenBDD one()
One
-BDD for this encoding.One
-BDDzero()
public final RavenBDD zero()
Zero
-BDD for this encoding.Zero
-BDDone()
public final RavenBDDDomain getCurrentStateDomain()
getSuccessorStateDomain()
public final RavenBDDDomain getSuccessorStateDomain()
getCurrentStateDomain()
public final RavenBDD getInterfaceEncodingBDD()
getStateEncodingBDD()
public final RavenBDD getStateEncodingBDD()
getInterfaceEncodingBDD()