| AbstractFSACreator |
An AbstractFSACreator is capable of creating various types of
finite state automata with propositional alphabet and labels on transitions.
|
| AcceptingRunFinder |
This class performs a double depth-first search to find accepting runs in an
ω-automaton with acceptance on states.
|
| Aperiodic |
This class provides methods to determine whether a classic finite state
automaton or a Büchi automaton is aperiodic, determine whether the
language recognized by the automaton is star-free.
|
| ClassicComplement |
This class provides a complementation construction for classic finite state
automata.
|
| Closure |
Take the closure of a finite state automaton.
|
| Complementation |
Uses the default complementation algorithm to complement a finite state
automaton.
|
| CompleteFSAGenerator |
This class provides a generator to generate finite state automata of a state
size and an alphabet size completely.
|
| Concatenation |
This class provides a method for concatenating a prefix automaton and a
suffix automaton.
|
| Configuration |
A configuration is a tuple (s, seq) where s is the current state and seq is
the status of the input sequence associated with s.
|
| ConfigurationAutomaton |
This class defines a configuration automaton for another automaton A on an
input sequence W.
|
| ConfigurationState |
This class defines states with configurations.
|
| Containment |
This is a class for checking containment between two Büchi automata.
|
| DBW2ComplementDCW |
This class provides a conversion from DBW to complement DCW.
|
| DCW2ComplementDBW |
This class provides a conversion from DCW to complement DBW.
|
| DCW2NBW |
This class provides a conversion from DCW to equivalent NBW.
|
| Determinization |
This class collects several methods for the determinization of a finite state
automaton.
|
| DMW2ComplementDMW |
This class provides a conversion from DMW to complement DMW.
|
| DMW2DBW |
This class provides an implementation of the conversion from a DMW to an
equivalent DBW in [Lawrence H.
|
| DMW2DPW |
This class provides a conversion from DMW to equivalent DPW [Berndt Farwer.
|
| DMW2DRW |
This class provides a conversion from DMW to equivalent DRW [Berndt Farwer.
|
| DMW2DSW |
This class provides a conversion from DMW to equivalent DSW [Berndt Farwer.
|
| DPW2ComplementDPW |
This class provides a conversion from DPW to complement DPW.
|
| DRW2ComplementDSW |
This class provides a conversion from DRW to complement DSW.
|
| DSW2ComplementDRW |
This class provides a conversion from DRW to complement DSW.
|
| Emptiness |
Checks if the language of a finite state automaton is empty or not.
|
| Emptiness.Result |
This class defines the result of an emptiness test.
|
| Equivalence |
An Equivalence object provides methods for checking the language
equivalence between two ω-automata that can be converted to equivalent
NBW.
|
| Equivalence.Result |
This class defines the result of an equivalence test.
|
| FSA |
An FSA is a finite state automaton, including nondeterministic
classic finite word automaton (NFW), nondeterministic Büchi word
automaton (NBW), nondeterministic co-Büchi word automaton (NCW),
nondeterministic generalized Büchi word automaton (NGBW),
nondeterministic Muller word automaton (NMW), nondeterministic Rabin word
automaton (NRW), nondeterministic Streett word automaton (NSW), and
nondeterministic parity word automaton (NPW).
|
| FSA2AltAutomaton |
This class provides a conversion from a finite state automaton with
acceptance on states to an equivalent alternating automaton in DNF.
|
| FSA2DBWByBK09 |
This class provides a conversion from an automaton (convertible to an NBW) to
equivalent DBW through DCW by the approach in [BK09].
|
| FSA2DBWByLandweber |
This class provides a conversion from an automaton (convertible to a DMW) to
equivalent DBW through DMW by the approach in [Lan69].
|
| FSA2Game |
This class provides a conversion from a deterministic automaton with a
propositional alphabet to a turn-based game.
|
| FSA2NMW |
This class provides a conversion from a finite state automaton to equivalent
NMW.
|
| FSAState |
An FSAState is no more than a normal State.
|
| FSATransition |
An FSATransition is no more than a normal
Transition.
|
| HOACreator |
A HOACreator is capable of creating a Hanoi omega-automaton with
labels on transitions.
|
| InputSequence |
An InputSequence is a string uvvv..., denoted by u{v}, where u
is a finite prefix and v is the infinite part.
|
| InputSimulator |
An InputSimulator takes an automaton and an input word as its
inputs and computes all runs of the automaton on the input word
incrementally.
|
| InputTester |
An InputTester tests if an input sequence is accepted by an automaton
or not.
|
| InputTester.AcceptingRunFinder |
This class is used to traverse a configuration automaton C of an
automaton A to find a lasso of C such that the corresponding lasso of A
is accepting.
|
| InputTester.Result |
This class defines the result of an input test.
|
| Intersection |
An Intersection provides methods for taking the intersection of
two classic finite state automata or two ω-automata.
|
| Intersection.NBWIntersectState |
This class defines states in the intersected NBW.
|
| Intersection.NFWIntersectState |
This class defines states in the intersected NFW.
|
| LabelPositionConverter |
A LabelPositionConverter can convert a label-on-state FSA (acceptance
condition on states) to a label-on-transition FSA.
|
| Minimization |
This class provides methods for the minimization of classic finite automata.
|
| NBW2ComplementUCW |
This class implements a conversion from NBW to complement UCW.
|
| NBW2DCW |
This class provides a conversion from an NBW B to a DCW C such that L(B)
⊆ L(C) and if B is DCW-recognizable, L(C) ⊆ L(B) [Udi Boker, Orna
Kupferman: Co-ing Büchi Made Tight and Useful.
|
| NBW2DPW |
This class provides a conversion from NBW to equivalent DPW.
|
| NBW2DRW |
This class provides a conversion from NBW to equivalent DRW.
|
| NBW2NCW |
This class provides a conversion from an NBW B to an NCW C such that L(B)
⊆ L(C) and if B is NCW-recognizable, L(C) ⊆ L(B) [Udi Boker, Orna
Kupferman: Co-ing Büchi Made Tight and Useful.
|
| NBW2NGBW |
This class provides a conversion from NBW to equivalent NGBW.
|
| NBW2NMW |
This class provides a conversion from NBW to equivalent NMW.
|
| NBW2NPW |
This class provides a conversion from NBW to equivalent NPW.
|
| NBW2NRW |
This class provides a conversion from NBW to equivalent NRW.
|
| NBW2NSW |
This class provides a conversion from NBW to equivalent NSW.
|
| NBW2NTBW |
This class provides a conversion from NBW to equivalent NTBW.
|
| NBW2SDBW |
This class provides a conversion from an NBW to an equivalent SDBW.
|
| NBWCreator |
An NBWCreator is capable of creating an NBW with propositional
alphabet and labels on transitions.
|
| NCW2ComplementUBW |
This class implements a conversion from NCW to complement UBW.
|
| NCW2DCW |
This class implements a conversion from NCW to DCW.
|
| NCW2NMW |
This class provides a conversion from NCW to equivalent NMW.
|
| NCWCreator |
An NCWCreator is capable of creating an NCW with propositional
alphabet and labels on transitions.
|
| NFW2DFW |
This class implements the standard determinization construction (subset
construction) of NFW.
|
| NFWCreator |
An NFWCreator is capable of creating an NFW with propositional
alphabet and labels on transitions.
|
| NGBW2NBW |
This class provides a conversion from NGBW to equivalent NBW.
|
| NGBW2NBWSet |
This class provides a conversion from NGBW to equivalent NBW.
|
| NGBW2NMW |
This class provides a conversion from NGBW to equivalent NMW.
|
| NGBWCreator |
An NGBWCreator is capable of creating an NGBW with propositional
alphabet and labels on transitions.
|
| NMW2NBW |
This class provides a conversion from NMW to equivalent NBW.
|
| NMWCreator |
An NMWCreator is capable of creating an NMW with propositional
alphabet and labels on transitions.
|
| NPW2NBW |
This class provides a conversion from NPW to equivalent NBW.
|
| NPW2NMW |
This class provides a conversion from NPW to equivalent NMW.
|
| NPW2NRW |
This class provides a conversion from NPW to equivalent NRW.
|
| NPW2NSW |
This class provides a conversion from NPW to equivalent NSW.
|
| NPWCreator |
An NPWCreator is capable of creating an NPW with propositional
alphabet and labels on transitions.
|
| NREWCreator |
An NREWCreator is capable of creating an NREW with propositional
alphabet and labels on transitions.
|
| NRW2NBW |
This class provides a conversion from NRW to equivalent NBW.
|
| NRW2NMW |
This class provides a conversion from NRW to equivalent NMW.
|
| NRWCreator |
An NRWCreator is capable of creating an NRW with propositional
alphabet and labels on transitions.
|
| NSW2NBW |
This class provides a conversion from NSW to equivalent NBW.
|
| NSW2NBW2 |
This class implements the conversion from an NSW to an NBW in [C.
|
| NSW2NGBW |
This class implements a conversion from an NSW to an NGBW.
|
| NSW2NMW |
This class provides a conversion from NSW to equivalent NMW.
|
| NSWCreator |
An NSWCreator is capable of creating an NSW with propositional
alphabet and labels on transitions.
|
| NTBW2NTGBW |
This class provides a conversion from NTBW to equivalent NTGBW.
|
| NTBWCreator |
An NTBWCreator is capable of creating an NTBW with propositional
alphabet and labels on transitions.
|
| NTGBW2NBW |
This class provides a conversion from NTGBW to equivalent NBW.
|
| NTGBW2NBWOptions |
This class provides options for the conversion from NTGBW to equivalent NBW.
|
| NTGBW2NGBW |
This class provides a conversion from NTGBW to equivalent NGBW.
|
| NTGBWCreator |
An NTGBWCreator is capable of creating an NTGBW with
propositional alphabet and labels on transitions.
|
| NTMWCreator |
An NTMWCreator is capable of creating an NTMW with propositional
alphabet and labels on transitions.
|
| NTPWCreator |
An NTPWCreator is capable of creating an NTPW with propositional
alphabet and labels on transitions.
|
| NTRWCreator |
An NTRWCreator is capable of creating an NTRW with propositional
alphabet and labels on transitions.
|
| NTSWCreator |
An NTSWCreator is capable of creating an NTSW with propositional
alphabet and labels on transitions.
|
| RandomFSA |
This is a generator of finite state automata.
|
| ReducedSplitTree |
This class provides methods to generate the reduced split tree of an NBW on
an input sequence.
|
| Replacement |
This class provides an implementation of string replacement based on [Fang
Yu, Tevfik Bultan, Marco Cova, Oscar H.
|
| ReverseNFW |
This class provides a conversion from an NFW A to another NFW
B such that B accepts the reverse of the language of
A.
|
| RunDag |
This class provides methods to generate the run DAG of an automaton on an
input sequence.
|
| RunTree |
This class provides methods to generate the run tree of an automaton on an
input sequence.
|
| SemanticDeterminism |
This class provides tests if an automaton is semantically deterministic.
|
| SemanticDeterminismByLandweber |
This class provides tests if an automaton is semantically deterministic, i.e.
|
| SimulationEquivalence |
Checks if two ω-automata with the same type of acceptance condition are
simulation equivalent.
|
| SimulationEquivalence.Result |
This class defines the result of the simulation equivalence test.
|
| SplitTree |
This class provides methods to generate the split tree of an NBW on an input
sequence.
|
| SplitTree.Node |
This class defines nodes in a split tree.
|
| Subset |
This class provides an implementation of subset construction of automata with
labels on transitions.
|
| TemporalHierarchyClassification |
This class provides a classification of automata and temporal formulae into
the temporal hierarchy.
|
| TransitionMonoid |
This class provides methods to construct a monoid from a classic finite state
automaton or a Büchi automaton.
|
| TransitionMonoid.ValueSemiring |
|
| Unambiguity |
This class provides methods to check if a Büchi automaton is ambiguous.
|
| Union |
Takes the union of two classic finite automata or two ω-automata that
can be converted to NBW.
|