All Classes Interface Summary Class Summary Enum Summary Exception Summary Annotation Types Summary
Class |
Description |
AbstractCachedStatesAutomaton<S,A extends OmegaAcceptance> |
|
AbstractImplicitAutomaton<S,A extends OmegaAcceptance> |
|
AcceptanceOptimizations |
|
AcceptanceOptimizations.AcceptanceOptimizationTransformer |
|
Aig |
|
AigConsumer |
|
AigerPrinter |
|
AigFactory |
|
AigPrintable |
|
AllAcceptance |
|
AnnotatedLDBA<S,T extends LtlLanguageExpressible,B extends GeneralizedBuchiAcceptance,X,Y> |
|
AnnotatedState<S> |
|
AnnotatedStateOptimisation |
|
AsymmetricEvaluatedFixpoints |
|
AsymmetricEvaluatedFixpoints.DeterministicAutomata |
|
AsymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance> |
|
AsymmetricProductState |
|
Automaton<S,A extends OmegaAcceptance> |
The base interface providing read access to an automaton.
|
Automaton.EdgeMapVisitor<S> |
|
Automaton.EdgeTreeVisitor<S> |
|
Automaton.EdgeVisitor<S> |
|
Automaton.PreferredEdgeAccess |
|
Automaton.Property |
|
Automaton.Visitor<S> |
|
AutomatonFactory |
|
AutomatonOperations |
|
AutomatonReader |
|
AutomatonReader.HoaState |
|
AutomatonUtil |
|
Biconditional |
Biconditional.
|
BinaryModalOperator |
|
BinaryVisitor<P,R> |
|
BlockingModalOperatorsVisitor |
|
BooleanConstant |
|
BooleanExpressions |
|
BreakpointState<E> |
|
BreakpointState<S> |
|
BuchiAcceptance |
|
BuchiDegeneralization |
|
CEntryPoint |
|
CoBuchiAcceptance |
|
Collections3 |
|
Conjunction |
|
Converter |
|
DaemonThreadFactory |
|
DecomposedDPA |
|
DecomposedDPA.Reference |
|
DeduplicationRewriter |
|
DefaultCli |
|
DelagBuilder |
|
DeterministicAutomaton<S,T> |
|
DeterministicConstructions |
|
DeterministicConstructions.CoSafety |
|
DeterministicConstructions.FgSafety |
|
DeterministicConstructions.GCoSafety |
|
DeterministicConstructions.GfCoSafety |
|
DeterministicConstructions.Safety |
|
DeterministicConstructions.Tracking |
|
Disjunction |
|
DPA2Safety<S> |
|
Edge<S> |
This class (with specialised subclasses) represents edges of automata including their acceptance
membership.
|
EdgeMapAutomatonMixin<S,A extends OmegaAcceptance> |
|
Edges |
|
EdgesAutomatonMixin<S,A extends OmegaAcceptance> |
|
EdgeTreeAutomatonMixin<S,A extends OmegaAcceptance> |
|
Either<A,B> |
|
EmersonLeiAcceptance |
|
Environment |
The environment makes global configuration available to all parts of the pipeline.
|
EquivalenceClass |
EquivalenceClass interface.
|
EquivalenceClassFactory |
|
EverythingIsNonnullByDefault |
|
ExternalTranslator |
|
Factories |
|
FactorySupplier |
|
FGX2DPA |
|
Fixpoints |
|
FOperator |
Finally.
|
Formula |
|
Formula.LogicalOperator |
|
Formula.ModalOperator |
|
Formula.TemporalOperator |
|
FormulaIsomorphism |
|
Formulas |
|
FrequencyG |
|
FrequencyG.Comparison |
|
FrequencyG.Limes |
|
Game<S,A extends OmegaAcceptance> |
|
Game.Owner |
|
GameFactory |
|
GameUtil |
|
GameViews |
|
GameViews.Node<S> |
A state of the split game.
|
GeneralizedBuchiAcceptance |
|
GeneralizedRabinAcceptance |
Generalized Rabin Acceptance - OR (Fin(i) and AND Inf(j)).
|
GeneralizedRabinAcceptance.Builder |
|
GeneralizedRabinAcceptance.RabinPair |
|
GeneralizedRabinAcceptanceOptimizations |
|
GenericConstructions |
|
GOperator |
Globally.
|
GuardedStream |
|
HashedTuple |
|
HoaPrinter |
|
HoaPrinter.HoaOption |
|
IARBuilder<R> |
|
IARState<R> |
|
ImplicitNonDeterministicEdgeTreeAutomaton<S,A extends OmegaAcceptance> |
|
InputReader |
Input readers are tasked with providing input to the processing pipeline.
|
InputReaders |
|
InputReaders.CheckedCallback |
|
IntBiConsumer |
|
IntVisitor |
|
JBddSupplier |
|
LabelledAig |
|
LabelledFormula |
|
LabelledSplit |
|
LabelledTree<L1,L2> |
|
LabelledTree.Leaf<L1,L2> |
|
LabelledTree.Node<L1,L2> |
|
LanguageAnalysis |
|
LanguageContainment |
|
LanguageEmptiness |
|
LanguageMembership |
|
LatexPrintVisitor |
|
LegacyFactory |
Deprecated. |
Literal |
|
LiteralMapper |
|
LiteralMapper.ShiftedFormula |
|
LTL2DAFunction |
|
LTL2DAFunction.Constructions |
|
LTL2DAModule |
|
LTL2DGRAModule |
|
LTL2DPAFunction |
|
LTL2DPAFunction.Configuration |
|
LTL2DPAModule |
|
LTL2DRAModule |
|
LTL2LDBAModule |
|
LTL2LDGBAModule |
|
LTL2NAFunction |
|
LTL2NAFunction.Constructions |
|
LTL2NAModule |
|
LTL2NBAModule |
|
LTL2NGBAModule |
|
LtlLanguageExpressible |
|
LTLLexer |
|
LtlParser |
|
LTLParser |
|
LTLParser.AndExpressionContext |
|
LTLParser.AtomExpressionContext |
|
LTLParser.BinaryExpressionContext |
|
LTLParser.BinaryOpContext |
|
LTLParser.BinaryOperationContext |
|
LTLParser.BinaryUnaryContext |
|
LTLParser.BoolContext |
|
LTLParser.BooleanContext |
|
LTLParser.ComparisonContext |
|
LTLParser.DoubleQuotedVariableContext |
|
LTLParser.ExpressionContext |
|
LTLParser.FormulaContext |
|
LTLParser.FractionContext |
|
LTLParser.FrequencyOpContext |
|
LTLParser.FrequencySpecContext |
|
LTLParser.NestedContext |
|
LTLParser.OrExpressionContext |
|
LTLParser.ProbabilityContext |
|
LTLParser.SingleQuotedVariableContext |
|
LTLParser.UnaryAtomContext |
|
LTLParser.UnaryExpressionContext |
|
LTLParser.UnaryOpContext |
|
LTLParser.UnaryOperationContext |
|
LTLParser.VariableContext |
|
LTLParserBaseListener |
This class provides an empty implementation of LTLParserListener ,
which can be extended to create a listener which only needs to handle a subset
of the available methods.
|
LTLParserBaseVisitor<T> |
This class provides an empty implementation of LTLParserVisitor ,
which can be extended to create a visitor which only needs to handle a subset
of the available methods.
|
LTLParserListener |
This interface defines a complete listener for a parse tree produced by
LTLParser .
|
LTLParserVisitor<T> |
This interface defines a complete generic visitor for a parse tree produced
by LTLParser .
|
Monitor<F extends UnaryModalOperator> |
|
MOperator |
Strong Release.
|
MutableAutomaton<S,A extends OmegaAcceptance> |
|
MutableAutomatonFactory |
|
MutableAutomatonUtil |
|
MutableAutomatonUtil.Sink |
|
NBA2DPA |
|
NBA2LDBA |
|
NBA2LDBA.LDBA<S> |
|
NonDeterministicConstructions |
|
NonDeterministicConstructions.CoSafety |
|
NonDeterministicConstructions.FgSafety |
|
NonDeterministicConstructions.GfCoSafety |
|
NonDeterministicConstructions.Safety |
|
NonDeterministicConstructions.Tracking |
|
NoneAcceptance |
|
NormalForms |
|
OmegaAcceptance |
|
OmegaAcceptanceOptimizations |
|
OutputWriter |
The final piece of every pipeline, formatting the produced results and writing them on some
output.
|
OutputWriter.Binding |
|
OutputWriters |
|
OutputWriters.AutomatonStats |
|
OutputWriters.ToHoa |
|
OwlModule |
|
OwlModuleParser<M extends OwlModule> |
|
OwlModuleParser.ReaderParser |
|
OwlModuleParser.TransformerParser |
|
OwlModuleParser.WriterParser |
|
OwlModuleRegistry |
A registry holding all modules used to parse the command line.
|
OwlModuleRegistry.OwlModuleNotFoundException |
|
OwlModuleRegistry.Type |
|
OwlParser |
|
ParityAcceptance |
|
ParityAcceptance.Parity |
|
ParityAcceptanceOptimizations |
|
ParityGameSolver |
|
ParityUtil |
|
PartialConfigurationParser |
Utility class used to parse a simplified command line (single exposed module with rest of the
pipeline preconfigured).
|
PartialModuleConfiguration |
|
PartialModuleConfiguration.Constructor |
|
Pipeline |
|
PipelineException |
|
PipelineExecutionContext |
Holds information about an execution originating from a particular input.
|
PipelineParser |
|
PipelineParser.ModuleParseException |
|
PipelineRunner |
Helper class to execute a specific pipeline with created input and output streams.
|
Predicates |
|
PrintVisitor |
|
ProductState |
|
PromisedSet |
|
PropositionalFormula |
|
PropositionalIntVisitor |
Visitor skeleton implementation that views the formula as propositional formula.
|
PropositionalVisitor<T> |
Visitor skeleton implementation that views the formula as propositional formula.
|
PullUpXVisitor |
|
PullUpXVisitor.XFormula |
|
RabinAcceptance |
This class represents a Rabin acceptance.
|
RabinAcceptance.Builder |
|
RabinDegeneralization |
|
RabinizerBuilder |
Central class handling the Rabinizer construction.
|
RabinizerConfiguration |
|
RabinizerState |
|
RankingState<S> |
|
Rewriter |
|
Rewriter.ToCoSafety |
|
Rewriter.ToSafety |
|
RobustLtlInputReader |
|
RobustLtlParser |
|
Robustness |
|
ROperator |
Weak Release.
|
RoundRobinState<E> |
|
RunUtil |
|
SafetyAutomaton |
|
SafetyCoreDetector |
|
SccDecomposition<S> |
Finds the SCCs of a given graph / transition system using Tarjan's algorithm.
|
Selector |
|
ServerCli |
|
ServerRunner |
|
SimplifierFactory |
|
SimplifierFactory.Mode |
|
SimplifierTransformer |
|
Split |
|
State<T> |
|
StringUtil |
|
SuccessorFunction<S> |
|
SymmetricDRAConstruction<R extends GeneralizedRabinAcceptance> |
|
SymmetricEvaluatedFixpoints |
|
SymmetricEvaluatedFixpoints.DeterministicAutomata |
|
SymmetricEvaluatedFixpoints.NonDeterministicAutomata |
|
SymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance> |
|
SymmetricNBAConstruction<B extends GeneralizedBuchiAcceptance> |
|
SymmetricProductState |
|
SyntacticFragment |
|
SyntacticFragments |
|
Synthesis |
|
TokenErrorListener |
|
Transformer |
Transformers are the central pieces of the pipeline concept.
|
Transformer.Instance |
|
Transformers |
|
Transformers.SimpleTransformer |
|
Tuple |
|
TwoPartAutomaton<A,B,C extends OmegaAcceptance> |
|
TypeUtil |
|
UltimatelyPeriodicWord |
|
UnabbreviateVisitor |
|
UnaryModalOperator |
|
UOperator |
Strong Until.
|
UpwardClosedSet |
Bucket-based implementation of an upward-closed set.
|
ValuationSet |
|
ValuationSetFactory |
|
ValuationTree<E> |
|
ValuationTree.Leaf<E> |
|
ValuationTree.Node<E> |
|
ValuationTrees |
|
Views |
|
Views.AutomatonView<S,A extends OmegaAcceptance> |
|
Visitor<R> |
|
WOperator |
Weak Until.
|
XDepthVisitor |
|
XOperator |
Next.
|