Package net.automatalib.modelchecking
Interface Lasso<I,D>
-
- Type Parameters:
I
- the input typeD
- the output type
- All Superinterfaces:
Automaton<Integer,I,Integer>
,DeterministicAutomaton<Integer,I,Integer>
,DeterministicTransitionSystem<Integer,I,Integer>
,DetOutputAutomaton<Integer,I,Integer,D>
,FiniteRepresentation
,InputAlphabetHolder<I>
,Iterable<Integer>
,Output<I,D>
,OutputAutomaton<Integer,I,Integer,D>
,SimpleAutomaton<Integer,I>
,SimpleDeterministicAutomaton<Integer,I>
,SimpleDTS<Integer,I>
,SimpleTS<Integer,I>
,TransitionSystem<Integer,I,Integer>
- All Known Subinterfaces:
Lasso.DFALasso<I>
,Lasso.MealyLasso<I,O>
- All Known Implementing Classes:
AbstractLasso
,DFALassoImpl
,MealyLassoImpl
public interface Lasso<I,D> extends DetOutputAutomaton<Integer,I,Integer,D>, InputAlphabetHolder<I>
A lasso is a single infinite word.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.
-
-
Nested Class Summary
Nested Classes Modifier and Type Interface Description static interface
Lasso.DFALasso<I>
A DFALasso is a lasso forDFA
s.static interface
Lasso.MealyLasso<I,O>
A MealyLasso is a lasso forMealyMachine
s.-
Nested classes/interfaces inherited from interface net.automatalib.automaton.DeterministicAutomaton
DeterministicAutomaton.FullIntAbstraction<T>, DeterministicAutomaton.IntAbstraction<T>, DeterministicAutomaton.StateIntAbstraction<I,T>
-
-
Method Summary
All Methods Instance Methods Abstract Methods Modifier and Type Method 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 beginning 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.-
Methods inherited from interface net.automatalib.automaton.Automaton
transitionGraphView
-
Methods inherited from interface net.automatalib.automaton.DeterministicAutomaton
fullIntAbstraction, fullIntAbstraction, stateIntAbstraction
-
Methods inherited from interface net.automatalib.ts.DeterministicTransitionSystem
getSuccessor, getSuccessors, getTransition, getTransitions
-
Methods inherited from interface net.automatalib.automaton.concept.InputAlphabetHolder
getInputAlphabet
-
Methods inherited from interface java.lang.Iterable
forEach, spliterator
-
Methods inherited from interface net.automatalib.automaton.concept.Output
computeOutput
-
Methods inherited from interface net.automatalib.automaton.simple.SimpleAutomaton
createDynamicStateMapping, createStaticStateMapping, getStates, iterator, size, stateIDs
-
Methods inherited from interface net.automatalib.ts.simple.SimpleDTS
getInitialState, getInitialStates, getState, getStates, getSuccessor, getSuccessors, getSuccessors
-
Methods inherited from interface net.automatalib.ts.simple.SimpleTS
getSuccessors
-
Methods inherited from interface net.automatalib.ts.TransitionSystem
getSuccessor, powersetView
-
-
-
-
Method Detail
-
getOutput
D getOutput()
Gets the finite representation of the output of the lasso.- Returns:
- the output type D.
-
getLoopBeginIndices
SortedSet<Integer> getLoopBeginIndices()
The sorted set containing some symbol indices after which the beginning state of the loop is visited.
-
getUnfolds
int getUnfolds()
Returns the number of times the loop is unfolded.The returned value is always greater than 0.
- Returns:
- the number of times the loop is unfolded.
-
getAutomaton
DetOutputAutomaton<?,I,?,D> getAutomaton()
Returns the original automaton from which this lasso is constructed.- Returns:
- the original automaton.
-
-