Package net.automatalib.modelchecking

Class AbstractLasso<I,D>

java.lang.Object

net.automatalib.modelchecking.AbstractLasso<I,D>

All Implemented Interfaces:

Iterable<Integer>, Automaton<Integer,I,Integer>, DetOutputAutomaton<Integer,I,Integer,D>, FiniteRepresentation, InputAlphabetHolder<I>, Output<I,D>, OutputAutomaton<Integer,I,Integer,D>, DeterministicAutomaton<Integer,I,Integer>, SimpleAutomaton<Integer,I>, SimpleDeterministicAutomaton<Integer,I>, Lasso<I,D>, DeterministicTransitionSystem<Integer,I,Integer>, SimpleDTS<Integer,I>, SimpleTS<Integer,I>, TransitionSystem<Integer,I,Integer>

Direct Known Subclasses:

DFALassoImpl, MealyLassoImpl

public abstract class AbstractLasso<I,D>
extends Object
implements Lasso<I,D>

Nested Class Summary

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

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

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.Lasso

Lasso.DFALasso<I>, Lasso.MealyLasso<I,O>

Field Summary

Fields

Modifier and Type	Field	Description
static String	NO_LASSO

Constructor Summary

Constructors

Constructor	Description
AbstractLasso(DetOutputAutomaton<S,I,?,D> automaton, Collection<? extends I> inputs, int unfoldTimes)	Constructs a finite representation of a given automaton (that contains a lasso), by unrolling the loop unfoldTimes.

Method Summary

Modifier and Type	Method	Description
DetOutputAutomaton<?,I,?,D>	getAutomaton()	Returns the original automaton from which this lasso is constructed.
Integer	getInitialState()	Retrieves the initial state of this transition system.
Alphabet<I>	getInputAlphabet()	Gets the input alphabet of this automaton.
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.
Collection<Integer>	getStates()	Retrieves all states of the transition system.
@Nullable Integer	getSuccessor(Integer state, I input)	Get the successor state of a given state, or null when no such successor exists.
@Nullable Integer	getTransition(Integer state, I input)	Retrieves the transition triggered by the given input symbol.
int	getUnfolds()	Returns the number of times the loop is unfolded.
Word<I>	getWord()	Gets the finite representation of the lasso.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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

getSuccessors, getTransitions

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, iterator, size, stateIDs

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

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

Field Detail

NO_LASSO

public static final String NO_LASSO

See Also:

Constant Field Values

Constructor Detail

AbstractLasso

public AbstractLasso(DetOutputAutomaton<S,I,?,D> automaton,
                     Collection<? extends I> inputs,
                     int unfoldTimes)

Constructs a finite representation of a given automaton (that contains a lasso), by unrolling the loop unfoldTimes.

Type Parameters:

S - the state type

Parameters:

automaton - the automaton containing the lasso.

inputs - the input alphabet.

unfoldTimes - the number of times the loop needs to be unrolled, must be > 0.

Method Detail

getAutomaton

public DetOutputAutomaton<?,I,?,D> getAutomaton()

Description copied from interface: Lasso

Returns the original automaton from which this lasso is constructed.

Specified by:

getAutomaton in interface Lasso<I,D>

Returns:

the original automaton.

getUnfolds

public int getUnfolds()

Description copied from interface: Lasso

Returns the number of times the loop is unfolded.

The returned value is always greater than 0.

Specified by:

getUnfolds in interface Lasso<I,D>

Returns:

the number of times the loop is unfolded.

getWord

public Word<I> getWord()

Description copied from interface: Lasso

Gets the finite representation of the lasso.

Specified by:

getWord in interface Lasso<I,D>

Returns:

the Word.

getLoop

public Word<I> getLoop()

Description copied from interface: Lasso

Gets the loop of the lasso.

Specified by:

getLoop in interface Lasso<I,D>

Returns:

the Word.

getPrefix

public Word<I> getPrefix()

Description copied from interface: Lasso

Gets the prefix of the lasso.

Specified by:

getPrefix in interface Lasso<I,D>

Returns:

the Word.

getOutput

public D getOutput()

Description copied from interface: Lasso

Gets the finite representation of the output of the lasso.

Specified by:

getOutput in interface Lasso<I,D>

Returns:

the output type D.

getLoopBeginIndices

public SortedSet<Integer> getLoopBeginIndices()

Description copied from interface: Lasso

The sorted set containing some symbol indices after which the beginning state of the loop is visited.

Specified by:

getLoopBeginIndices in interface Lasso<I,D>

getInitialState

public Integer getInitialState()

Description copied from interface: SimpleDTS

Retrieves the initial state of this transition system.

Specified by:

getInitialState in interface SimpleDTS<I,D>

Returns:

the initial state.

See Also:

SimpleTS.getInitialStates()

getSuccessor

public @Nullable Integer getSuccessor(Integer state,
                                      I input)

Get the successor state of a given state, or null when no such successor exists.

Specified by:

getSuccessor in interface DeterministicTransitionSystem<Integer,I,Integer>

Specified by:

getSuccessor in interface SimpleDTS<I,D>

Parameters:

state - the source state.

input - the input symbol.

Returns:

the successor state reachable by the given input symbol, or null if no state is reachable by this symbol.

See Also:

SimpleDTS.getSuccessor(Object, Object)

getStates

public Collection<Integer> getStates()

Description copied from interface: SimpleAutomaton

Retrieves all states of the transition system. Implementing classes should return an unmodifiable collection

Specified by:

getStates in interface SimpleAutomaton<I,D>

Returns:

all states in the transition system

getInputAlphabet

public Alphabet<I> getInputAlphabet()

Gets the input alphabet of this automaton.

Specified by:

getInputAlphabet in interface InputAlphabetHolder<I>

Returns:

the Alphabet.

getTransition

public @Nullable Integer getTransition(Integer state,
                                       I input)

Description copied from interface: DeterministicTransitionSystem

Retrieves the transition triggered by the given input symbol.

Specified by:

getTransition in interface DeterministicTransitionSystem<Integer,I,Integer>

Parameters:

state - the source state.

input - the input symbol.

Returns:

the transition triggered by the given input symbol, or null if no transition is triggered.

See Also:

TransitionSystem.getTransitions(Object, Object)