public final class UnionEncoding extends BDDEncoding
UnionAutomaton
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 UnionEncoding |
getEncoding(Automaton first,
Automaton second)
Returns the default BDD encoding for a union of two automata.
|
Automaton |
getFirstAutomaton()
Returns the first automaton.
|
Automaton |
getSecondAutomaton()
Returns the second automaton.
|
RavenBDD |
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 . |
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 UnionEncoding getEncoding(Automaton first, Automaton second)
first
- the first automaton to be used for the union encodingsecond
- the second automaton to be used for the union encodingpublic RavenBDD getSeparationBit(BDDEncoding.StateType type)
state
the separation bit has been set if
and only if the BDD is true
.type
- the state type, either current state or successor statepublic 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