Package net.automatalib.modelchecking
Class DFALassoImpl<I>
- java.lang.Object
-
- net.automatalib.modelchecking.AbstractLasso<I,Boolean>
-
- net.automatalib.modelchecking.DFALassoImpl<I>
-
- Type Parameters:
I
- the input type
- All Implemented Interfaces:
Iterable<Integer>
,Automaton<Integer,I,Integer>
,DetOutputAutomaton<Integer,I,Integer,Boolean>
,DetSuffixOutputAutomaton<Integer,I,Integer,Boolean>
,FiniteRepresentation
,InputAlphabetHolder<I>
,Output<I,Boolean>
,OutputAutomaton<Integer,I,Integer,Boolean>
,SuffixOutput<I,Boolean>
,DeterministicAutomaton<Integer,I,Integer>
,DFA<Integer,I>
,FiniteStateAcceptor<Integer,I>
,NFA<Integer,I>
,SimpleAutomaton<Integer,I>
,SimpleDeterministicAutomaton<Integer,I>
,UniversalAutomaton<Integer,I,Integer,Boolean,Void>
,UniversalDeterministicAutomaton<Integer,I,Integer,Boolean,Void>
,Lasso<I,Boolean>
,Lasso.DFALasso<I>
,AcceptorTS<Integer,I>
,DeterministicAcceptorTS<Integer,I>
,DeterministicTransitionSystem<Integer,I,Integer>
,SimpleDTS<Integer,I>
,SimpleTS<Integer,I>
,TransitionSystem<Integer,I,Integer>
,UniversalDTS<Integer,I,Integer,Boolean,Void>
,UniversalTransitionSystem<Integer,I,Integer,Boolean,Void>
public class DFALassoImpl<I> extends AbstractLasso<I,Boolean> implements Lasso.DFALasso<I>
A DFALasso is a lasso forDFA
s.
-
-
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.automaton.fsa.FiniteStateAcceptor
FiniteStateAcceptor.FSAGraphView<S,I,A extends FiniteStateAcceptor<S,I>>
-
Nested classes/interfaces inherited from interface net.automatalib.modelchecking.Lasso
Lasso.DFALasso<I>, Lasso.MealyLasso<I,O>
-
Nested classes/interfaces inherited from interface net.automatalib.automaton.UniversalDeterministicAutomaton
UniversalDeterministicAutomaton.FullIntAbstraction<T,SP,TP>, UniversalDeterministicAutomaton.IntAbstraction<T,SP,TP>, UniversalDeterministicAutomaton.StateIntAbstraction<I,T,SP,TP>
-
-
Field Summary
-
Fields inherited from class net.automatalib.modelchecking.AbstractLasso
NO_LASSO
-
Fields inherited from interface net.automatalib.automaton.fsa.FiniteStateAcceptor
STATE_PROPERTIES, TRANSITION_PROPERTIES
-
-
Constructor Summary
Constructors Constructor Description DFALassoImpl(DetOutputAutomaton<?,I,?,Boolean> automaton, Collection<? extends I> inputs, int unfoldTimes)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description boolean
isAccepting(Integer state)
Returns whether the given state is accepting.-
Methods inherited from class net.automatalib.modelchecking.AbstractLasso
getAutomaton, getInitialState, getInputAlphabet, getLoop, getLoopBeginIndices, getOutput, getPrefix, getStates, getSuccessor, getTransition, getUnfolds, getWord
-
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
-
Methods inherited from interface net.automatalib.ts.acceptor.AcceptorTS
getStateProperty, getSuccessor, getTransitionProperty
-
Methods inherited from interface net.automatalib.ts.DeterministicTransitionSystem
getSuccessor, getSuccessors, getTransition, getTransitions
-
Methods inherited from interface net.automatalib.automaton.fsa.DFA
accepts, computeOutput, computeStateOutput, computeSuffixOutput, isAccepting
-
Methods inherited from interface net.automatalib.automaton.fsa.FiniteStateAcceptor
transitionGraphView
-
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.modelchecking.Lasso
getAutomaton, getLoop, getLoopBeginIndices, getOutput, getPrefix, getUnfolds, getWord
-
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
powersetView
-
Methods inherited from interface net.automatalib.automaton.UniversalDeterministicAutomaton
fullIntAbstraction, fullIntAbstraction, stateIntAbstraction
-
Methods inherited from interface net.automatalib.ts.UniversalDTS
getTransitionProperty
-
-
-
-
Constructor Detail
-
DFALassoImpl
public DFALassoImpl(DetOutputAutomaton<?,I,?,Boolean> automaton, Collection<? extends I> inputs, int unfoldTimes)
-
-
Method Detail
-
isAccepting
public boolean isAccepting(Integer state)
Returns whether the given state is accepting.The current state is only accepting iff it is precisely the state after the last symbol index in the finite representation of the lasso.
- Specified by:
isAccepting
in interfaceAcceptorTS<Integer,I>
- Parameters:
state
- to compute whether it is accepting.- Returns:
- whether the given
state
is accepting.
-
-