I
- the input typeD
- the output typepublic interface Lasso<I,D> extends DetOutputAutomaton<Integer,I,Integer,D>, InputAlphabetHolder<I>
The implementation is an automaton such that its singleton language is the infinite word. Also, the implementation is actually the finite representation (by unrolling the loop) of the infinite word, including information how many times the loop of the lasso is unrolled.
Modifier and Type | Interface and Description |
---|---|
static interface |
Lasso.DFALasso<I>
A DFALasso is a lasso for
DFA s. |
static interface |
Lasso.MealyLasso<I,O>
A MealyLasso is a lasso for
MealyMachine s. |
DeterministicAutomaton.FullIntAbstraction<T>, DeterministicAutomaton.IntAbstraction<T>, DeterministicAutomaton.StateIntAbstraction<I,T>
Modifier and Type | Method and Description |
---|---|
DetOutputAutomaton<?,I,?,D> |
getAutomaton()
Returns the original automaton from which this lasso is constructed.
|
Word<I> |
getLoop()
Gets the loop of the lasso.
|
SortedSet<Integer> |
getLoopBeginIndices()
The sorted set containing some symbol indices after which the begin state of the loop is visited.
|
D |
getOutput()
Gets the finite representation of the output of the lasso.
|
Word<I> |
getPrefix()
Gets the prefix of the lasso.
|
int |
getUnfolds()
Returns the number of times the loop is unfolded.
|
Word<I> |
getWord()
Gets the finite representation of the lasso.
|
computeOutput
fullIntAbstraction, fullIntAbstraction, stateIntAbstraction
transitionGraphView
createDynamicStateMapping, createStaticStateMapping, getStates, iterator, size, stateIDs
forEach, spliterator
getSuccessor, getSuccessors, getTransition, getTransitions, transToSet
getSuccessor, powersetView
getInitialState, getInitialStates, getState, getStates, getSuccessor, getSuccessors, stateToSet
getSuccessors
getInputAlphabet
D getOutput()
SortedSet<Integer> getLoopBeginIndices()
int getUnfolds()
DetOutputAutomaton<?,I,?,D> getAutomaton()
Copyright © 2020. All rights reserved.