net.automatalib.modelchecking

Interface Lasso<I,D>

Type Parameters:

I - the input type

D - the output type

All Superinterfaces:

Automaton<Integer,I,Integer>, DeterministicAutomaton<Integer,I,Integer>, DeterministicTransitionSystem<Integer,I,Integer>, DetOutputAutomaton<Integer,I,Integer,D>, 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

@ParametersAreNonnullByDefault
public interface Lasso<I,D>
extends DetOutputAutomaton<Integer,I,Integer,D>, InputAlphabetHolder<I>

A lasso is an 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.

Author:

Jeroen Meijer

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static interface	Lasso.DFALasso<I> A DFALasso is a lasso for DFAs.
static interface	Lasso.MealyLasso<I,O> A MealyLasso is a lasso for MealyMachines.

Nested classes/interfaces inherited from interface net.automatalib.automata.DeterministicAutomaton

DeterministicAutomaton.FullIntAbstraction<T>, DeterministicAutomaton.IntAbstraction<T>, DeterministicAutomaton.StateIntAbstraction<I,T>

Method Summary

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.

Methods inherited from interface net.automatalib.automata.concepts.Output

computeOutput

Methods inherited from interface net.automatalib.automata.DeterministicAutomaton

fullIntAbstraction, fullIntAbstraction, stateIntAbstraction

Methods inherited from interface net.automatalib.automata.Automaton

transitionGraphView

Methods inherited from interface net.automatalib.automata.simple.SimpleAutomaton

createStaticStateMapping, getStates, iterator, size, stateIDs

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Methods inherited from interface net.automatalib.ts.DeterministicTransitionSystem

getSuccessor, getSuccessors, getTransition, getTransitions, transToSet

Methods inherited from interface net.automatalib.ts.TransitionSystem

getSuccessor, powersetView

Methods inherited from interface net.automatalib.ts.simple.SimpleDTS

getInitialState, getInitialStates, getState, getStates, getSuccessor, getSuccessors, stateToSet

Methods inherited from interface net.automatalib.ts.simple.SimpleTS

createDynamicStateMapping, getSuccessors

Methods inherited from interface net.automatalib.automata.concepts.InputAlphabetHolder

getInputAlphabet

Method Detail

getWord

Word<I> getWord()

Gets the finite representation of the lasso.

Returns:

the Word.

getLoop

Word<I> getLoop()

Gets the loop of the lasso.

Returns:

the Word.

getPrefix

Word<I> getPrefix()

Gets the prefix of the lasso.

Returns:

the Word.

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 begin 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

@Nullable
DetOutputAutomaton<?,I,?,D> getAutomaton()

Returns the original automaton from which this lasso is constructed.

Returns:

the original automaton.