public final class ProductEncoding extends BDDEncoding
ProductAutomaton
BDDEncoding.StateType
Modifier and Type | Method and Description |
---|---|
RavenBDD |
convertFinalStates(Automaton automaton)
Converts the final state set of the given automaton to the
UnionEncoding . |
RavenBDD |
convertInitialStates(Automaton automaton)
Converts the initial state set of the given automaton to the
UnionEncoding . |
RavenBDD |
convertNonFinalStates(Automaton automaton)
Converts the non-final state set of the given automaton to the
UnionEncoding . |
RavenBDD |
convertStates(Automaton automaton)
Converts the state set of the given automaton to the
UnionEncoding . |
RavenBDD |
convertTransitions(Automaton automaton,
Operation letter)
Converts the transitions of the given automaton and the given letter to the
UnionEncoding . |
String |
getBitType(int pos)
Returns a string indicating which information is encoded by bit of the given position
pos . |
static ProductEncoding |
getEncoding(Automaton first,
Automaton second)
Returns the default BDD encoding for a product of two BDD encodings.
|
Automaton |
getFirstAutomaton()
Returns the first automaton.
|
Automaton |
getSecondAutomaton()
Returns the second automaton.
|
String |
printStates(RavenBDD stateSet)
Prints a single state (seen as singleton state set) or a set of states.
|
getBit, getCurrentStateDomain, getInnerInterface, getInterfaceBit, getInterfaceEncodingBDD, getInterfaceLength, getInterfaceSize, getInterfaceSizeIsGreaterOrEqual, getInterfaceSizeIsLessOrEqual, getInterfaceSizeType, getLength, getMaximumInterface, getOuterInterface, getStateBit, getStateEncodingBDD, getStateLength, getStateType, getSuccessorStateDomain, one, toString, zero
public static final ProductEncoding getEncoding(Automaton first, Automaton second)
first
- the first encoding to be used for the product encodingsecond
- the second encoding to be used for the product 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 printedpublic Automaton getFirstAutomaton()
public Automaton getSecondAutomaton()
public RavenBDD convertStates(Automaton automaton)
UnionEncoding
.automaton
- the automaton whose states are to be converted (must either be the first or
the second automaton of the UnionEncoding
public RavenBDD convertInitialStates(Automaton automaton)
UnionEncoding
.automaton
- the automaton whose states are to be converted (must either be the first or
the second automaton of the UnionEncoding
public RavenBDD convertFinalStates(Automaton automaton)
UnionEncoding
.automaton
- the automaton whose states are to be converted (must either be the first or
the second automaton of the UnionEncoding
public RavenBDD convertNonFinalStates(Automaton automaton)
UnionEncoding
.automaton
- the automaton whose states are to be converted (must either be the first or
the second automaton of the UnionEncoding
public RavenBDD convertTransitions(Automaton automaton, Operation letter)
UnionEncoding
.automaton
- the automaton whose transitions are to be converted (must either be the first
or the second automaton of the UnionEncoding
letter
- the letter which indicates the transition