public abstract class Automaton extends Object implements Data, Cloneable, Serializable
Modifier and Type | Class and Description |
---|---|
static class |
Automaton.Type
Enumeration of the different types of implemented automata.
|
Modifier and Type | Field and Description |
---|---|
static String |
AUTOMATON_MAIN_FILE |
static String |
FINAL_STATES_FILE |
static String |
INITIAL_STATES_FILE |
static String |
NON_FINAL_STATES_FILE |
static String |
STATES_FILE |
Modifier and Type | Method and Description |
---|---|
void |
addComputationListener(ComputationListener l)
Adds the Computation Listener
l to this automaton. |
abstract Automaton |
clone() |
boolean |
containsInitialState(RavenBDD stateSet)
Returns
true if the state set stateSet contains at least one
initial state. |
Signature |
getAlphabet()
Returns the alphabet of this automaton.
|
RavenBDD |
getCurrentInterfaceSize(RavenBDD states)
Returns the interface size of the states in the given state set
states . |
BDDEncoding |
getEncoding()
Returns the BDD encoding used by this automaton.
|
RavenBDD |
getFinalStates()
Returns the final state set encoded as an BDD.
|
RavenBDD |
getInitialStates()
Returns the initial state set encoded as an BDD.
|
int |
getInnerInterface()
Returns the size of the inner interface of this automaton.
|
static RavenBDDPairing |
getInterfacePairing(Automaton first,
Automaton second)
Returns a BDD pairing which pairs the the interface bits of the two
automata
first and second . |
LinkedList<ComputationListener> |
getListener()
Returns the listener; For saving purposes only
|
Logger |
getLogger()
Returns the logger; For saving purposes only
|
int |
getMaximumInterface()
Returns the maximum interface of this automaton.
|
RavenBDD |
getNonFinalStates()
Returns the non-final state set encoded as an BDD.
|
RavenBDD |
getNonFinalStates(int size)
Returns the set of non-final states for the interface of size
size encoded as an BDD. |
int |
getNumberOfFinalStates()
Returns the number of final states of this automaton.
|
int |
getNumberOfInitialStates()
Returns the number of initial states of this automaton.
|
int |
getNumberOfNonFinalStates()
Returns the number of non-final states of this automaton.
|
int |
getNumberOfNonFinalStates(int size)
Returns the number of non-final states of this automaton for the given
interface size
size . |
int |
getNumberOfStates()
Returns the number of all states of this automaton.
|
int |
getNumberOfStates(int size)
Returns the number of states of this automaton for the given interface
size
size . |
int |
getOuterInterface()
Returns the size of the outer interface of this automaton.
|
RavenBDD |
getPredecessorStates(RavenBDD currentStates,
Operation letter)
Returns the set of predecessor states for a given set of current states
and and a given input letter (i.e. a graph operation).
|
RavenBDD |
getReachableStates(CospanDecomposition decomposition)
Returns the set of reachable states for a given graph decomposition
starting with the initial states.
|
int |
getSize()
Returns the size of the automaton (in the number of BDD nodes used to
encode the state set)
|
String |
getStateName(RavenBDD state)
Returns the state name of a single state encoded as bdd.
|
RavenBDD |
getStates()
Returns the state set encoded as an BDD.
|
RavenBDD |
getStates(int size)
Returns the state set for the interface of size
size encoded as an BDD. |
RavenBDD |
getStatesWithoutSuccessorFor(Operation letter)
Returns the set of states which have no successor state for the given
letter |
Map<Operation,RavenBDD> |
getStateTransBDDs()
Returns the Transition BDD Map For saving purposes only
|
RavenBDD |
getSuccessorStates(RavenBDD currentStates,
Operation letter)
Returns the set of successor states for a given set of current states and
and a given input letter (i.e. a graph operation).
|
RavenBDD |
getTransitionRelation(Operation letter)
Returns the transition relation for the given letter
|
Automaton.Type |
getType()
Returns the type of the data object.
|
void |
initializeEncoding() |
boolean |
isAcceptingStateSet(RavenBDD stateSet)
Returns
true if the state set stateSet is a subset of the
final state set. |
boolean |
isApplicable(Operation letter,
RavenBDD states)
Returns
true if the letter letter is applicable to the
states states , i.e. there exists at least one successor state
according to the transition relation for the letter letter . |
boolean |
isInitialStateSet(RavenBDD stateSet)
Returns
true if the state set stateSet is a subset of the
initial state set. |
String |
printStates(RavenBDD stateSet)
Prints a single state (seen as singleton state set) or a set of states.
|
void |
readAutomatonFromZip(String zipname)
Restores all transient attributes of the automaton.
|
void |
removeComputationListener(ComputationListener l)
Remove the Computation Listener
l from this automaton. |
String |
toString() |
void |
writeAutomatonToZip(String filename)
This method is called when an object of the class Automaton shall be
saved.
|
public static final String AUTOMATON_MAIN_FILE
public static final String STATES_FILE
public static final String INITIAL_STATES_FILE
public static final String FINAL_STATES_FILE
public static final String NON_FINAL_STATES_FILE
public static final RavenBDDPairing getInterfacePairing(Automaton first, Automaton second)
first
and second
.first
- the first automatonsecond
- the second automatonpublic abstract Automaton clone() throws CloneNotSupportedException
clone
in class Object
CloneNotSupportedException
public void addComputationListener(ComputationListener l)
l
to this automaton.l
- the listener to receive computation eventspublic void removeComputationListener(ComputationListener l)
l
from this automaton.l
- the listener which has been registered beforepublic final Automaton.Type getType()
Data
public final int getMaximumInterface()
public final int getInnerInterface()
public final int getOuterInterface()
public final Signature getAlphabet()
public final Logger getLogger()
public final LinkedList<ComputationListener> getListener()
public void initializeEncoding()
public final BDDEncoding getEncoding()
public final int getSize()
public final void writeAutomatonToZip(String filename) throws IOException
filename
- the name of the fileIOException
- thrown if an I/O error occurredpublic final void readAutomatonFromZip(String zipname) throws IOException
zipname
- the name of the zip archiveIOException
- thrown if an I/O error occurredpublic final String getStateName(RavenBDD state)
state
- the bdd encoding the statepublic final RavenBDD getStates()
public final RavenBDD getStates(int size)
size
encoded as an BDD.size
- the size of the interfacesize
-th state setpublic final Map<Operation,RavenBDD> getStateTransBDDs()
public final boolean isInitialStateSet(RavenBDD stateSet)
true
if the state set stateSet
is a subset of the
initial state set.stateSet
- the set of statestrue
if the state set contains only initial states,
false
otherwisegetInitialStates()
,
isAcceptingStateSet(RavenBDD)
public final int getNumberOfStates()
public final int getNumberOfStates(int size)
size
.size
- the size of the interfacepublic final RavenBDD getInitialStates()
public final int getNumberOfInitialStates()
public final boolean isAcceptingStateSet(RavenBDD stateSet)
true
if the state set stateSet
is a subset of the
final state set.stateSet
- the set of statestrue
if the state set contains only final states,
false
otherwisegetFinalStates()
,
isInitialStateSet(RavenBDD)
public final boolean containsInitialState(RavenBDD stateSet)
true
if the state set stateSet
contains at least one
initial state.stateSet
- the set of statestrue
if the state set contains at least one initial state,
false
otherwisegetInitialStates()
,
isInitialStateSet(RavenBDD)
public final RavenBDD getFinalStates()
public final int getNumberOfFinalStates()
public final RavenBDD getNonFinalStates()
public final RavenBDD getNonFinalStates(int size)
size
encoded as an BDD.size
- the size of the interfacesize
-th set of non-final statespublic final int getNumberOfNonFinalStates()
public final int getNumberOfNonFinalStates(int size)
size
.size
- the size of the interfacepublic final boolean isApplicable(Operation letter, RavenBDD states)
true
if the letter letter
is applicable to the
states states
, i.e. there exists at least one successor state
according to the transition relation for the letter letter
.letter
- the input letterstates
- the current statestrue
if the letter is applicable, false
otherwisegetTransitionRelation(Operation)
,
getSuccessorStates(RavenBDD, Operation)
public final RavenBDD getTransitionRelation(Operation letter)
letter
- the letter for which the transition relation is returnedpublic final RavenBDD getCurrentInterfaceSize(RavenBDD states)
states
.states
- the state setpublic final RavenBDD getReachableStates(CospanDecomposition decomposition)
decomposition
- the input graph decompositionpublic final RavenBDD getSuccessorStates(RavenBDD currentStates, Operation letter)
currentStates
- the current statesletter
- the input letterpublic final RavenBDD getPredecessorStates(RavenBDD currentStates, Operation letter)
currentStates
- the current statesletter
- the input letterpublic final RavenBDD getStatesWithoutSuccessorFor(Operation letter)
letter
letter
- the letter for which the transition function is checkedpublic final String printStates(RavenBDD stateSet)
stateSet
- the state set to be printedBDDEncoding.printStates(RavenBDD)