| AbstractAcc<T extends GraphicComponent,S extends AbstractGraphicComponentSet<T,S>,L extends AbstractGraphicComponentList<T,S,L>,R extends Run<T,L>,A extends AbstractAcc<T,S,L,R,A>> |
This class provides acceptance conditions on either states or transitions but
not both.
|
| AbstractGraphicComponentList<T extends GraphicComponent,S extends AbstractGraphicComponentSet<T,S>,L extends AbstractGraphicComponentList<T,S,L>> |
This class provides a list of graphic components.
|
| AbstractGraphicComponentSet<T extends GraphicComponent,S extends AbstractGraphicComponentSet<T,S>> |
This class provides an ordered set containing graphic components.
|
| AbstractListPairSetAcc<T extends GraphicComponent,S extends AbstractGraphicComponentSet<T,S>,L extends AbstractGraphicComponentList<T,S,L>,R extends Run<T,L>,A extends AbstractListPairSetAcc<T,S,L,R,A>> |
This class provides a category of acceptance conditions of which eac
condition is a set {(E1, F1), ..., (En, Fn)} of pairs where Ei and Fi are
sets of states or transitions.
|
| AbstractListSetAcc<T extends GraphicComponent,S extends AbstractGraphicComponentSet<T,S>,L extends AbstractGraphicComponentList<T,S,L>,R extends Run<T,L>,A extends AbstractListSetAcc<T,S,L,R,A>> |
This class provides a category of acceptance conditions of which each
condition contains a list of acceptance sets {F1, F2, ..., Fn} of states or
transitions.
|
| AbstractNBWLikeAcc<A extends AbstractNBWLikeAcc<A>> |
This class provides a category of acceptance conditions of which each
condition is a set of states.
|
| AbstractNGBWLikeAcc<A extends AbstractNGBWLikeAcc<A>> |
This class provides a category of acceptance conditions which contains a list
of acceptance sets {F1, F2, ..., Fn} of states.
|
| AbstractNRWLikeAcc<A extends AbstractNRWLikeAcc<A>> |
This class provides a category of acceptance conditions of which eac
condition is a set {(E1, F1), ..., (En, Fn)} of pairs where Ei and Fi are
sets of states.
|
| AbstractNTBWLikeAcc<A extends AbstractNTBWLikeAcc<A>> |
This is a category of acceptance conditions similar to
AbstractNBWLikeAcc but the acceptance condition is on
transitions.
|
| AbstractNTGBWLikeAcc<A extends AbstractNTGBWLikeAcc<A>> |
This is a category of acceptance conditions similar to
AbstractNGBWLikeAcc but the acceptance condition is on
transitions.
|
| AbstractNTRWLikeAcc<A extends AbstractNTRWLikeAcc<A>> |
This class provides a category of acceptance conditions of which eac
condition is a set {(E1, F1), ..., (En, Fn)} of pairs where Ei and Fi are
sets of transitions.
|
| AbstractRandomAutomaton<T extends Automaton> |
This is a generator of random automata.
|
| AbstractSetAcc<T extends GraphicComponent,S extends AbstractGraphicComponentSet<T,S>,L extends AbstractGraphicComponentList<T,S,L>,R extends Run<T,L>,A extends AbstractSetAcc<T,S,L,R,A>> |
This class provides a category of acceptance conditions of which each
condition is a set of states or transitions.
|
| Acc<R extends Run<?,?>> |
This class defines some common parts of acceptance conditions.
|
| AcceptanceAtom |
An AcceptanceAtom is an atomic element in the Boolean condition of a
general acceptance condition.
|
| AcceptanceCondition.Renderer |
This class provides a list cell renderer for acceptance conditions.
|
| AcceptanceProperty |
This class provides a derived property for the acceptance of a state or
transition in an automaton.
|
| AccEvent |
An AccEvent is an automaton event indicating a change on an
acceptance condition.
|
| AlphabetAbstraction |
This class provides a method to abstract the alphabet of an automaton that
has
a propositional alphabet,
labels on transitions, and
an acceptance condition on states.
The original propositions of the automaton will be replaced by new
propositions defined as predicates of the original propositions.
|
| Automaton |
An Automaton object contains a finite alphabet, a finite set of
states, a finite set of transitions, and an acceptance condition.
|
| AutomatonComparator |
This class sorts automata ascendantly by the state size and the transition
size.
|
| AutomatonComponent |
An AutomatonComponent is a component of an automaton, for example,
states, transitions, and acceptance conditions.
|
| AutomatonEvent |
An AutomatonEvent indicates a change on an automaton.
|
| BuchiAcc |
A Büchi acceptance condition is a set of states.
|
| ChainedConversion |
This class provides a conversion from a source automaton type to a target
automaton type through other automaton types.
|
| ClassicAcc |
A classic acceptance condition is a set of states.
|
| CoBuchiAcc |
A co-Büchi acceptance condition is a set of states.
|
| ContainmentResult<T> |
This class defines the result of a containment test.
|
| DFS |
This class provides depth-first searches (DFS) in an automaton.
|
| DFSTraverser |
Deprecated.
|
| DoubleDFS |
This class provides double depth-first searches in an automaton for finding
accepting lassos.
|
| DoubleDFSTraverser |
Deprecated.
|
| EditableTransferable |
This class provides a transferable object for editable objects.
|
| ElementaryCycleFinder |
|
| ElementaryCycleGenerator |
This class provides an implementation of the algorithm in [Donald B.
|
| GeneralizedBuchiAcc |
A generalized Büchi acceptance condition is a list {F0, F1, ..., Fn}
where Fi's are sets of states.
|
| GraphicComponent |
This class defines components in an automaton that appear as a graph.
|
| GraphicComponentComparator<T extends GraphicComponent> |
A GraphicComponentComparator compares two graphic components.
|
| GraphicComponentList |
This class provides lists of graphic components.
|
| GraphicComponentMap<T extends GraphicComponent> |
This class provides a map from an ID to a graphic component.
|
| GraphicComponentRun |
This class defines runs composed of states and transitions.
|
| GraphicComponentSet |
A GraphicComponentSet is an ordered set.
|
| HanoiAcc |
This class provides an implementation of a Hanoi acceptance condition, which
contains
a Boolean expression over AcceptanceAtom, and
a list of acceptance sets, of which each acceptance set has a unique
ID.
|
| LassoFinder |
The lasso finder can find all lassos on an automaton.
|
| LiteralStringComparator |
A LiteralComparator compares literals alphabetically.
|
| Morphism |
This class provides methods for checking homomorphism and isomorphism between
two automata.
|
| MSCCFinder |
This class provides methods to find maximal strongly connected components
(MSCCs) in an automaton.
|
| MullerAcc |
A Muller acceptance condition is a list {F0, F1, ..., Fn} where Fi's are sets
of states.
|
| OmegaUtil |
This class provides several utility methods for ω-automata.
|
| OmegaUtil.CycleFinder |
A CycleFinder is able to find all elementary cycles of an
automaton.
|
| ParityAcc |
A parity acceptance condition is a list {F0, F1, F2, ..., Fn} where Fi's are
state sets.
|
| Product |
This class provide an implementation of taking the product of two automata.
|
| RabinAcc |
A Rabin acceptance condition is a list {(E0, F0), (E1, F1), ..., (En,Fn)}
where Ei's and Fi's are state sets.
|
| RandomAutomaton<T extends Automaton> |
This is a generator of random automata.
|
| ReachabilityAcc |
This class defines reachability acceptance conditions.
|
| SetEvent<T> |
A SetEvent is an event that indicates changes of a set.
|
| State |
A state contains a unique identifier, a name, a label, and some other
properties.
|
| StateComparator |
A StateComparator compares two states based on their IDs.
|
| StateEvent |
A StateEvent is an automaton event that indicates a change on a
state.
|
| StateList |
A StateList is a sequence of states.
|
| StateMap |
A StateMap is a map of a state ID to a state of the ID.
|
| StateRun |
A StateRun is a possibly infinite state sequence.
|
| StateSet |
A StateSet is a set of states ordered ascendantly by their IDs.
|
| StreettAcc |
A Streett acceptance condition is a list {(E0, F0), (E1, F1), ..., (En,Fn)}
where Ei's and Fi's are state sets.
|
| StructureType |
This class defines types of structures.
|
| TBuchiAcc |
A TBuchiAcc is a transitional Büchi acceptance condition,
which is a set of transitions.
|
| TCoBuchiAcc |
A TCoBuchiAcc is a transitional co-Büchi acceptance
condition, which is a set of transitions.
|
| TGeneralizedBuchiAcc |
A TGeneralizedBuchiAcc is a transitional generalized Büchi
acceptance condition.
|
| TMullerAcc |
A TMullerAcc is a transitional Muller acceptance condition.
|
| TParityAcc |
A TParityAcc is a transitional parity acceptance condition.
|
| TRabinAcc |
A TRabinAcc is a transitional Rabin acceptance condition.
|
| Transition |
A transition is a direct edge from a source state to a destination state.
|
| TransitionComparator |
This class defines a comparator which sorts transitions by comparing the
source states first, then the destination states, the transition labels, and
finally transition IDs.
|
| TransitionEvent |
A TransitionEvent is an automaton event that indicates a change
on a transition.
|
| TransitionList |
A TransitionList is a sequence of transitions.
|
| TransitionRun |
A TransitionRun is a possibly infinite transition sequence.
|
| TransitionSet |
A TransitionSet is a set of transitions ordered ascendantly by
their IDs.
|
| TStreettAcc |
A TStreettAcc is a transitional Streett acceptance condition.
|