public abstract class AbstractLasso<I,D> extends Object implements Lasso<I,D>
Lasso.DFALasso<I>, Lasso.MealyLasso<I,O>
DeterministicAutomaton.FullIntAbstraction<T>, DeterministicAutomaton.IntAbstraction<T>, DeterministicAutomaton.StateIntAbstraction<I,T>
Constructor and 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 . |
Modifier and Type | Method and 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 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.
|
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.
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
computeOutput
fullIntAbstraction, fullIntAbstraction, stateIntAbstraction
transitionGraphView
createDynamicStateMapping, createStaticStateMapping, iterator, size, stateIDs
forEach, spliterator
getSuccessors, getTransitions, transToSet
getSuccessor, powersetView
getInitialStates, getState, getStates, getSuccessor, getSuccessors, stateToSet
getSuccessors
public static final String NO_LASSO
public AbstractLasso(DetOutputAutomaton<S,I,?,D> automaton, Collection<? extends I> inputs, int unfoldTimes)
unfoldTimes
.S
- the state typeautomaton
- the automaton containing the lasso.inputs
- the input alphabet.unfoldTimes
- the number of times the loop needs to be unrolled, must be > 0
.public DetOutputAutomaton<?,I,?,D> getAutomaton()
Lasso
getAutomaton
in interface Lasso<I,D>
public int getUnfolds()
Lasso
getUnfolds
in interface Lasso<I,D>
public Word<I> getWord()
Lasso
public Word<I> getLoop()
Lasso
public Word<I> getPrefix()
Lasso
public D getOutput()
Lasso
public SortedSet<Integer> getLoopBeginIndices()
Lasso
getLoopBeginIndices
in interface Lasso<I,D>
public Integer getInitialState()
SimpleDTS
getInitialState
in interface SimpleDTS<Integer,I>
SimpleTS.getInitialStates()
public @Nullable Integer getSuccessor(Integer state, I input)
null
when no such successor exists.getSuccessor
in interface DeterministicTransitionSystem<Integer,I,Integer>
getSuccessor
in interface SimpleDTS<Integer,I>
state
- the source state.input
- the input symbol.null
if no state is reachable by
this symbol.SimpleDTS.getSuccessor(Object, Object)
public Collection<Integer> getStates()
SimpleAutomaton
getStates
in interface SimpleAutomaton<Integer,I>
public Alphabet<I> getInputAlphabet()
getInputAlphabet
in interface InputAlphabetHolder<I>
public @Nullable Integer getTransition(Integer state, I input)
DeterministicTransitionSystem
getTransition
in interface DeterministicTransitionSystem<Integer,I,Integer>
state
- the source state.input
- the input symbol.null
if no transition is triggered.TransitionSystem.getTransitions(Object, Object)
Copyright © 2020. All rights reserved.