All Classes

Class	Description
AbstractAutomatonGraphView<S,A extends Automaton<S,?,?>,E>
AcceptanceGraph<N,E>	Interface for finite graphs that embody the concept of node acceptance.
AcceptorTS<S,I>	A transition system whose semantics are defined by whether a state is "accepting" or not.
ADSNode<S,I,O>	A (simplified) node in an adaptive distinguishing sequence.
Alphabet<I>	Class implementing an (indexed) alphabet.
AutomataLibLocalPropertiesSource
AutomataLibPropertiesSource
AutomataLibProperty	An enum of all the system properties currently used by AutomataLib.
AutomataLibSettings
AutomataLibSettingsSource
AutomataLibSystemPropertiesSource
Automaton<S,I,T>	Basic interface for an automaton.
AutomatonCreator<A,I>
AutomatonGraphView<S,I,T,A extends Automaton<S,I,T>>
AutomatonVisualizationHelper<S,I,T,A extends Automaton<S,I,T>>
BidirectionalGraph<N,E>	Interface for bidirectional graph.
BidirectionalGraph.IntAbstraction<E>	Interface for node integer abstractions of a BidirectionalGraph.
CFMPSGraphView<N,L,E,AP>	Graph representation of a ContextFreeModalProcessSystem that displays all nodes of its sub-procedures once, i.e., without incorporating execution semantics such as expansion.
CFMPSVisualizationHelper<N,L,E>
ContextFreeModalProcessSystem<L,AP>	Represents a Context-Free Modal Transition System as defined in the paper M3C: Modal Meta Model Checking.
DefaultVisualizationHelper<N,E>
DeterministicAbstractions	Default implementations for DeterministicAutomaton abstractions.
DeterministicAbstractions.FullIntAbstraction<I,T,A extends DeterministicAutomaton.StateIntAbstraction<I,T>>
DeterministicAbstractions.StateIntAbstraction<S,I,T,A extends DeterministicAutomaton<S,I,T>>
DeterministicAcceptorTS<S,I>	A deterministic acceptor transition system.
DeterministicAutomaton<S,I,T>	Basic interface for a deterministic automaton.
DeterministicAutomaton.FullIntAbstraction<T>	Interface for full integer abstractions of a DeterministicAutomaton.
DeterministicAutomaton.IntAbstraction<T>	Base interface for integer abstractions of a DeterministicAutomaton.
DeterministicAutomaton.StateIntAbstraction<I,T>	Interface for state integer abstractions of a DeterministicAutomaton.
DeterministicOutputTS<S,I,T,O>
DeterministicStateOutputTS<S,I,T,O>
DeterministicTransitionOutputTS<S,I,T,O>
DeterministicTransitionSystem<S,I,T>	Deterministic transition system.
DetOutputAutomaton<S,I,T,D>	An automaton which deterministically produces an output for an input word.
DetSuffixOutputAutomaton<S,I,T,D>
DFA<S,I>	Deterministic finite state acceptor.
DirectPowersetDTS<S,I,T>
EdgeLabels<E,L>	Edge label context, for Graphs with labeled edges.
EdgeWeights<E>	Edge weights concepts.
FinalNode<N>
FiniteAlphabetAutomaton<S,I,T>
FiniteKripkeStructure<N,E,AP>	A Kripke structure is a graph which has sets of atomic properties assigned to its nodes.
FiniteKTS<S,I,T,AP>	A finite Kripke Transition System combines the properties of a finite transition system and a KripkeInterpretation.
FiniteLabeledGraph<N,E,L>
FiniteRepresentation	This interface marks automata types that have a finite representation, i.e. can be represented by a finite number of entities.
FiniteStateAcceptor<S,I>	FiniteStateAcceptors accept regular languages.
FiniteStateAcceptor.FSAGraphView<S,I,A extends FiniteStateAcceptor<S,I>>
FSAVisualizationHelper<S,I>
Graph<N,E>	Graph interface.
Graph.IntAbstraction<E>	Interface for node integer abstractions of a Graph.
GraphViewable
GrowingAlphabet<I>	Alphabet class that supports adding new symbols.
GrowingAlphabetNotSupportedException	An exception to be thrown when functionality revolving around GrowingAlphabet.addSymbol(Object) is accessed (e.g. by trying to add an alphabet symbol to an automaton) but the given data structure was not properly set up (e.g.
IndefiniteGraph<N,E>	Interface for an (indefinite) graph structure.
IndefiniteSimpleGraph<N>	A simplified interface for indefinite graphs, exposing only adjacency information, but no further information about edge objects.
InitialNode<N>	Initial node concept.
InputAlphabetHolder<I>
KripkeInterpretation<N,AP>	A Kripke interpretation for a graph.
Lasso<I,D>	A lasso is a single infinite word.
Lasso.DFALasso<I>	A DFALasso is a lasso for DFAs.
Lasso.MealyLasso<I,O>	A MealyLasso is a lasso for MealyMachines.
MealyMachine<S,I,T,O>
MealyMachine.MealyGraphView<S,I,T,O,A extends MealyMachine<S,I,T,O>>
MealyTransitionSystem<S,I,T,O>
MealyVisualizationHelper<S,I,T,O>
ModalEdgeProperty
ModalEdgeProperty.ModalType
ModalTransitionSystem<S,I,T,TP extends ModalEdgeProperty>	A modal transition system is a UniversalAutomaton in which transitions can be marked as may or must edges.
ModalTransitionSystem.MTSGraphView<S,I,T,TP extends ModalEdgeProperty,M extends ModalTransitionSystem<S,I,T,TP>>
ModelChecker<I,A,P,R>	A model-checker checks whether a given automaton satisfies a given property.
ModelChecker.DFAModelChecker<I,P,R>
ModelChecker.MealyModelChecker<I,O,P,R>	A model checker for Mealy machines.
ModelCheckerCache<I,A,P,R>	A model checker that caches calls to ModelChecker.findCounterExample(Object, Collection, Object).
ModelCheckerCache.DFAModelCheckerCache<I,P,R>
ModelCheckerCache.MealyModelCheckerCache<I,O,P,R>
ModelCheckerLasso<I,A,P,R extends Lasso<I,?>>	A model checker where the counterexample is a lasso.
ModelCheckerLasso.DFAModelCheckerLasso<I,P>
ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>
ModelCheckerLassoCache<I,A,P,R extends Lasso<I,?>>
ModelCheckerLassoCache.DFAModelCheckerLassoCache<I,P>
ModelCheckerLassoCache.MealyModelCheckerLassoCache<I,O,P>
ModelCheckingException	An Exception that may occur during model checking.
MooreMachine<S,I,T,O>
MooreMachine.MooreGraphView<S,I,T,O,A extends MooreMachine<S,I,T,O>>
MooreTransitionSystem<S,I,T,O>
MooreVisualizationHelper<S,I,T,O>
MTSVisualizationHelper<S,I,T,TP extends ModalEdgeProperty,M extends ModalTransitionSystem<S,I,T,TP>>
MutableAutomaton<S,I,T,SP,TP>	A mutable automaton.
MutableDeterministic<S,I,T,SP,TP>	Interface for a mutable deterministic automaton.
MutableDeterministic.FullIntAbstraction<T,SP,TP>	Interface for full integer abstractions of a MutableDeterministic.
MutableDeterministic.IntAbstraction<T,SP,TP>	Base interface for integer abstractions of a MutableDeterministic.
MutableDeterministic.StateIntAbstraction<I,T,SP,TP>	Interface for state integer abstractions of a MutableDeterministic.
MutableDeterministicAbstraction	Default implementations for MutableDeterministic abstractions.
MutableDeterministicAbstraction.FullIntAbstraction<I,T,SP,TP,A extends MutableDeterministic.StateIntAbstraction<I,T,SP,TP>>
MutableDeterministicAbstraction.StateIntAbstraction<S,I,T,SP,TP,A extends MutableDeterministic<S,I,T,SP,TP>>
MutableDFA<S,I>
MutableEdgeLabels<E,L>
MutableFSA<S,I>
MutableGraph<N,E,NP,EP>	A graph that allows modification.
MutableGraph.IntAbstraction<E,NP,EP>	Interface for node integer abstractions of a MutableGraph.
MutableKripkeInterpretation<N,AP>
MutableMealyMachine<S,I,T,O>
MutableModalEdgeProperty
MutableModalTransitionSystem<S,I,T,TP extends MutableModalEdgeProperty>	A mutable version of ModalTransitionSystem that allows to add states and transitions.
MutableMooreMachine<S,I,T,O>
MutableNFA<S,I>
MutableProbabilistic<T>
MutableProbabilisticMealy<S,I,T,O>
MutableProceduralModalEdgeProperty
MutableProceduralModalProcessGraph<N,L,E,AP,TP extends MutableProceduralModalEdgeProperty>	A mutable version of the ProceduralModalProcessGraph.
MutableStateOutput<S,O>
MutableSubsequentialTransducer<S,I,T,O>	A mutable extension of a SubsequentialTransducer.
MutableTransitionOutput<T,O>
MutableUniversalBidirectionalGraph<N,E,NP,EP>
NFA<S,I>	Nondeterministic finite state acceptor.
NodeAcceptance<N>	Node acceptance concept, for Graphs that represent a structure for deciding acceptance or rejection.
NodeIDs<N>	An interface for translating between graph nodes and their primitive representations as integers.
OneSEVPA<L,I>	A specialized interface for 1-SEVPAs (1-module single entry visibly push-down automata).
Output<I,D>	Feature for automata that compute an output.
OutputAutomaton<S,I,T,D>
PMPGVisualizationHelper<N,E,AP>
PowersetViewTS<S,I,T,OS,OT>
Probabilistic<T>
ProbabilisticMealyMachine<S,I,T,O>
ProbabilisticOutput<O>
ProceduralGraphView<S,I>	Graph representation of a ProceduralSystem that displays all states of its sub-procedures once, i.e., without incorporating execution semantics such as stack contents.
ProceduralInputAlphabet<I>	A specialized version of a VPAlphabet that is tailored towards procedural systems.
ProceduralModalEdgeProperty
ProceduralModalEdgeProperty.ProceduralType
ProceduralModalProcessGraph<N,L,E,AP,TP extends ProceduralModalEdgeProperty>	Represents a Procedural Modal Transition System as defined in the paper M3C: Modal Meta Model Checking.
ProceduralOutputAlphabet<O>	A specialized Alphabet for procedural systems that combines a regular output alphabet with a designated error symbol.
ProceduralVisualizationHelper<S,I>	Default VisualizationHelper for procedural systems.
RecursiveADSNode<S,I,O,N extends RecursiveADSNode<S,I,O,N>>	An interface representing a node in an adaptive distinguishing sequence (which essentially forms a decision tree).
SBA<S,I>	A system of behavioral automata.
SEVPA<L,I>	Interface for k-SEVPAs (k-module single entry visibly push-down automata), a visibly push-down automaton of specific structure and semantics.
SEVPAGraphView<L,I>
SEVPAGraphView.SevpaViewEdge<S,I>
ShrinkableAutomaton<S,I,T,SP,TP>	A mutable automaton that also supports destructive modifications, i.e., removal of states and transitions.
ShrinkableDeterministic<S,I,T,SP,TP>	A mutable deterministic automaton that also supports destructive operations, i.e., removal of states and transitions.
ShrinkableGraph<N,E>	A graph that supports (desirably efficient) removal of nodes and edges.
SimpleAutomaton<S,I>	A simple automaton, i.e., a SimpleTS with a finite number of states.
SimpleDeterministicAbstractions	Default implementations for SimpleDeterministicAutomaton abstractions.
SimpleDeterministicAbstractions.FullIntAbstraction<I,A extends SimpleDeterministicAutomaton.StateIntAbstraction<I>>	Base class implementing the default way of obtaining a SimpleDeterministicAbstractions.FullIntAbstraction, i.e., building on top of a SimpleDeterministicAbstractions.StateIntAbstraction and a mapping from integers to (concrete) input symbols.
SimpleDeterministicAbstractions.IntAbstraction<S,A extends SimpleDeterministicAutomaton<S,?>>	Base class implementing the default way of obtaining an integer abstraction from an automaton, i.e., by mapping states to integers and vice versa using the StateIDs mapping obtained via SimpleAutomaton.stateIDs().
SimpleDeterministicAbstractions.StateIntAbstraction<S,I,A extends SimpleDeterministicAutomaton<S,I>>	Base class implementing the default way of obtaining a SimpleDeterministicAutomaton.StateIntAbstraction.
SimpleDeterministicAutomaton<S,I>	A simple deterministic automaton.
SimpleDeterministicAutomaton.FullIntAbstraction	Interface for an integer abstraction that abstracts both states and input symbols to integers.
SimpleDeterministicAutomaton.IntAbstraction	Basic interface for integer abstractions of automata.
SimpleDeterministicAutomaton.StateIntAbstraction<I>	Interface for integer abstractions of an automaton that operate on non-abstracted input symbols (i.e., input symbols are of type I).
SimpleDTS<S,I>	A simple deterministic transition system.
SimpleGraph<N>	The finite version of a IndefiniteSimpleGraph.
SimpleGraph.IntAbstraction	Basic interface for integer abstractions of graphs.
SimpleNodeIDs<N>
SimpleStateIDs<S>
SimpleTS<S,I>	A simple transition system.
SPA<S,I>	A system of procedural automata.
SPMM<S,I,T,O>	A system of procedural Mealy machines.
SSTVisualizationHelper<S,I,T,O>
StackContents	A simplified stack implementation that allows to store integer values.
State<L>	Utility class to combine an entity (e.g. a location) with stack information.
StateAsNodeIDs<S>
StateIDGrowingMapping<S,V>
StateIDs<S>	An interface for translating between automaton states and their primitive representations as integers.
StateIDStaticMapping<S,V>
StateLocalInput<S,I>	Concept for transition systems, that can for each state return the set of input symbols for which successor states are defined.
StateLocalInputMealyMachine<S,I,T,O>
StateOutput<S,O>	State output concept.
StateOutputAutomaton<S,I,T,O>
SubsequentialTransducer<S,I,T,O>	A subsequential transducer (or SST) is an DeterministicOutputTS whose state and transition properties are output-words.
SubsequentialTransducer.SSTGraphView<S,I,T,O,A extends SubsequentialTransducer<S,I,T,O>>
SuffixOutput<I,D>	Feature for automata that compute a suffix-observable output function, i.e., they compute an output containing a part that can be attributed to a suffix of the input.
SupportsGrowingAlphabet<I>	Interface for declaring that a data structure supports adding new alphabet symbols after its instantiation.
TransitionEdge<I,T>
TransitionEdge.Property<I,TP>
TransitionOutput<T,O>	Transition output concept.
TransitionOutputAutomaton<S,I,T,O>
TransitionPredicate<S,I,T>
TransitionSystem<S,I,T>	Transition system interface.
UndefinedPropertyAccessException	This specialized exception can be thrown if during the traversal of an automaton or transition system an undefined property (e.g. a state or a transition output) is accessed, that is otherwise required for returning a valid result.
UndirectedGraph<N,E>	An undirected graph.
UniversalAutomaton<S,I,T,SP,TP>	A universal automaton is a generalized representation of automata, with unified access to the properties of states and transitions.
UniversalAutomatonGraphView<S,I,T,SP,TP,A extends UniversalAutomaton<S,I,T,SP,TP>>
UniversalBidirectionalGraph<N,E,NP,EP>
UniversalDeterministicAbstractions	Default implementations for UniversalDeterministicAutomaton abstractions.
UniversalDeterministicAbstractions.FullIntAbstraction<I,T,SP,TP,A extends UniversalDeterministicAutomaton.StateIntAbstraction<I,T,SP,TP>>
UniversalDeterministicAbstractions.StateIntAbstraction<S,I,T,SP,TP,A extends UniversalDeterministicAutomaton<S,I,T,SP,TP>>
UniversalDeterministicAutomaton<S,I,T,SP,TP>	A DeterministicAutomaton with state and transition properties.
UniversalDeterministicAutomaton.FullIntAbstraction<T,SP,TP>	Interface for full integer abstractions of a UniversalDeterministicAutomaton.
UniversalDeterministicAutomaton.IntAbstraction<T,SP,TP>	Base interface for integer abstractions of a UniversalDeterministicAutomaton.
UniversalDeterministicAutomaton.StateIntAbstraction<I,T,SP,TP>	Interface for state integer abstractions of a UniversalDeterministicAutomaton.
UniversalDTS<S,I,T,SP,TP>	Universal deterministic transition system.
UniversalFiniteAlphabetAutomaton<S,I,T,SP,TP>
UniversalGraph<N,E,NP,EP>
UniversalGraph.IntAbstraction<E,NP,EP>	Interface for node integer abstractions of a UniversalGraph.
UniversalIndefiniteGraph<N,E,NP,EP>	A universal graph, i.e., with (possibly empty) node and edge properties.
UniversalTransitionSystem<S,I,T,SP,TP>	A "universal" transition system, which captures the possibility to assign properties to states and transitions.
VisualizationHelper<N,E>	Helper interface for providing additional styling properties for plotting graphs.
VisualizationHelper.CommonAttrs
VisualizationHelper.CommonStyles
VisualizationHelper.EdgeAttrs
VisualizationHelper.EdgeStyles
VisualizationHelper.MTSEdgeAttrs
VisualizationHelper.NodeAttrs
VisualizationHelper.NodeShapes
VisualizationHelper.NodeStyles
VPAlphabet<I>	Alphabet definition for visible push-down automata.
VPAlphabet.SymbolType	Classifies an input symbol either as a call symbol, an internal symbol, or a return symbol.
Word<I>	A word is an ordered sequence of symbols.
WordBuilder<I>	A class for dynamically building Words.