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>
-
-
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 loopunfoldTimes
.
-
Method Summary
All Methods Instance Methods Concrete Methods 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, ornull
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 loopunfoldTimes
.- 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 interfaceLasso<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 interfaceLasso<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.
-
getLoop
public Word<I> getLoop()
Description copied from interface:Lasso
Gets the loop of the lasso.
-
getPrefix
public Word<I> getPrefix()
Description copied from interface:Lasso
Gets the prefix of the lasso.
-
getOutput
public D getOutput()
Description copied from interface:Lasso
Gets the finite representation of the output of the lasso.
-
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 interfaceLasso<I,D>
-
getInitialState
public Integer getInitialState()
Description copied from interface:SimpleDTS
Retrieves the initial state of this transition system.- Specified by:
getInitialState
in interfaceSimpleDTS<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, ornull
when no such successor exists.- Specified by:
getSuccessor
in interfaceDeterministicTransitionSystem<Integer,I,Integer>
- Specified by:
getSuccessor
in interfaceSimpleDTS<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 interfaceSimpleAutomaton<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 interfaceInputAlphabetHolder<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 interfaceDeterministicTransitionSystem<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)
-
-