All Classes Interface Summary Class Summary Enum Summary Exception Summary Annotation Types Summary
Class |
Description |
AbstractImmutableAutomaton<S,A extends OmegaAcceptance> |
This abstract class implements storage and retrieval of commonly fixed values, and overrides the
default implementations for Automaton.states() , Automaton.accept(Visitor) in
order to cache the set of reachable states for later use.
|
AbstractImmutableAutomaton.NonDeterministicEdgeMapAutomaton<S,A extends OmegaAcceptance> |
This class provides a skeleton implementation to create a non-deterministic on-the-fly
constructed automaton that uses ValuationSet as the main
representation of the transition relation.
|
AbstractImmutableAutomaton.NonDeterministicEdgesAutomaton<S,A extends OmegaAcceptance> |
This class provides a skeleton implementation to create a non-deterministic on-the-fly
constructed automaton.
|
AbstractImmutableAutomaton.NonDeterministicEdgeTreeAutomaton<S,A extends OmegaAcceptance> |
This class provides a skeleton implementation to create a non-deterministic on-the-fly
constructed automaton that uses ValuationTree as the main
representation of the transition relation.
|
AbstractImmutableAutomaton.SemiDeterministicEdgesAutomaton<S,A extends OmegaAcceptance> |
This class provides a skeleton implementation to create a semi-deterministic on-the-fly
constructed automaton.
|
AcceptanceOptimizations |
|
AcceptanceOptimizations.AcceptanceOptimizationTransformer |
|
Aig |
|
AigConsumer |
|
AigerPrinter |
|
AigFactory |
|
AigPrintable |
|
AllAcceptance |
|
AnnotatedLDBA<S,T extends LtlLanguageExpressible,B extends GeneralizedBuchiAcceptance,X,Y> |
Translation-specific internal representation of LDBAs.
|
AnnotatedState<S> |
|
AnnotatedStateOptimisation |
|
ArraysSupport |
|
AsymmetricEvaluatedFixpoints |
|
AsymmetricEvaluatedFixpoints.DeterministicAutomata |
|
AsymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance> |
|
AsymmetricProductState |
|
AsymmetricRankingState |
|
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> |
|
AutomatonUtil |
|
AutomatonUtil.LimitDeterministicGeneralizedBuchiAutomaton<S,B extends GeneralizedBuchiAcceptance> |
|
BackwardDirectSimulation<S> |
|
Biconditional |
Biconditional.
|
BinaryVisitor<P,R> |
|
BitSetUtil |
Utility functions to convert from and to bitsets.
|
BlockingElements |
|
BooleanConstant |
|
BooleanExpressions |
|
BooleanOperations |
This class provides standard boolean operations (union, intersection) on automata.
|
BreakpointState<S> |
|
BuchiAcceptance |
|
BuchiDegeneralization |
This class provides a conversion from generalised Büchi automata into Büchi automata.
|
BuchiDegeneralization.IndexedState<S> |
|
BuchiSimulation |
|
BuchiSimulationArguments |
|
CAutomaton |
|
CAutomaton.Acceptance |
|
CDecomposedDPA |
|
CDecomposedDPA.RealizabilityStatus |
|
CDecomposedDPA.Structure |
|
CDecomposedDPA.Structure.NodeType |
|
CDoubleArrayList |
|
CIntArrayList |
|
CInterface |
|
CLabelledFormula |
|
CLabelledFormula.AtomicPropositionStatus |
|
CoBuchiAcceptance |
|
Collections3 |
|
ColorRefinement<S> |
Computes direct simulation relation of an automaton based on the color refinement algorithm.
|
ColorRefinement.Neighborhood |
Represents the neighborhood of a state.
|
ColorRefinement.NeighborType |
Represents a neighbor type consisting of color and associated valuation.
|
CombinationGenerator |
|
CombineUntilVisitor |
|
Conjunction |
|
Converter |
|
DecomposedDPA |
|
DeduplicationRewriter |
|
DefaultCli |
|
DelagBuilder |
|
DeterministicConstructions |
|
DeterministicConstructions.BreakpointStateAccepting |
|
DeterministicConstructions.BreakpointStateRejecting |
|
DeterministicConstructions.CoSafety |
|
DeterministicConstructions.CoSafetySafety |
|
DeterministicConstructions.GfCoSafety |
|
DeterministicConstructions.Safety |
|
DeterministicConstructions.SafetyCoSafety |
|
DeterministicConstructions.Tracking |
|
DeterministicConstructionsPortfolio<A extends OmegaAcceptance> |
|
Determinization |
|
Determinization.BreakpointState<S> |
|
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> |
|
Either.Type |
|
EmersonLeiAcceptance |
|
EmptyAutomaton<S,A extends OmegaAcceptance> |
|
EmulatedCDoublePointer |
|
EmulatedCIntPointer |
|
Environment |
The environment makes global configuration available to all parts of the pipeline.
|
EquivalenceClass |
A propositional equivalence class of an LTL formula.
|
EquivalenceClassFactory |
A factory for creating propositional equivalence classes for LTL formulas.
|
EverythingIsNonnullByDefault |
|
ExternalTranslator |
|
ExternalTranslator.InputMode |
|
Factories |
|
FactorySupplier |
|
Fixpoints |
|
FOperator |
Finally.
|
Formula |
|
Formula.BinaryTemporalOperator |
|
Formula.NaryPropositionalOperator |
|
Formula.PropositionalOperator |
|
Formula.TemporalOperator |
|
Formula.UnaryTemporalOperator |
|
FormulaIsomorphism |
|
Formulas |
|
ForwardDelayedSimulation<S> |
|
ForwardDirectLookaheadSimulation<S> |
|
ForwardDirectSimulation<S> |
Simulation type for forward-direct multipebble simulation games.
|
ForwardFairSimulation<S> |
|
Game<S,A extends OmegaAcceptance> |
|
Game.Owner |
|
GameFactory |
|
GameUtil |
|
GameViews |
|
GameViews.Node<S> |
A state of the split game.
|
GeneralizedBuchiAcceptance |
|
GeneralizedCoBuchiAcceptance |
|
GeneralizedRabinAcceptance |
Generalized Rabin Acceptance - OR (Fin(i) and AND Inf(j)).
|
GeneralizedRabinAcceptance.Builder |
|
GeneralizedRabinAcceptance.RabinPair |
|
GeneralizedRabinAcceptanceOptimizations |
|
GenericConstructions |
|
GfgCoBuchiMinimization |
This class implements [ICALP'19] minimization of GFG automata.
|
GOperator |
Globally.
|
GuardedStream |
|
HashMapAutomaton<S,A extends OmegaAcceptance> |
|
HoaReader |
|
HoaReader.HoaState |
|
HoaWriter |
|
HoaWriter.HoaOption |
|
IARBuilder<R> |
|
IARState<R> |
|
InputReaders |
|
IntVisitor |
|
JBddSupplier |
|
LabelledAig |
|
LabelledFormula |
|
LabelledSplit |
|
LanguageAnalysis |
|
LanguageContainment |
|
LanguageEmptiness |
|
LanguageMembership |
|
LatexPrintVisitor |
|
LegacyFactory |
Deprecated. |
Literal |
|
LiteralMapper |
|
LiteralMapper.ShiftedLabelledFormula |
|
LTL2DAFunction |
|
LTL2DAModule |
|
LTL2DGRAModule |
|
LTL2DPAFunction |
|
LTL2DPAFunction.Configuration |
|
LTL2DPAModule |
|
LTL2DRAModule |
|
LTL2LDBAModule |
|
LTL2LDGBAModule |
|
LTL2NAFunction |
|
LTL2NAModule |
|
LTL2NBAModule |
|
LTL2NGBAModule |
|
LTL2NormalFormModule |
|
LtlfParser |
|
LtlfToLtlTranslator |
|
LtlfToLtlTranslator.LtlfToLtlVisitor |
|
LtlfToLtlTranslator.LtlfToLtlVisitor.PushNegOneDownVisitor |
|
LtlLanguageExpressible |
|
LTLLexer |
|
LtlParser |
|
LTLParser |
|
LTLParser.AndExpressionContext |
|
LTLParser.AtomExpressionContext |
|
LTLParser.BinaryExpressionContext |
|
LTLParser.BinaryOpContext |
|
LTLParser.BinaryOperationContext |
|
LTLParser.BinaryUnaryContext |
|
LTLParser.BoolContext |
|
LTLParser.BooleanContext |
|
LTLParser.DoubleQuotedVariableContext |
|
LTLParser.ExpressionContext |
|
LTLParser.FormulaContext |
|
LTLParser.NestedContext |
|
LTLParser.OrExpressionContext |
|
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 .
|
MonitorState |
|
MOperator |
Strong Release.
|
MultiPebble<S> |
Abstracts multiple pebbles controlled by Duplicator in a multipebble simulation game.
|
MutableAutomaton<S,A extends OmegaAcceptance> |
|
MutableAutomatonUtil |
|
MutableAutomatonUtil.Sink |
|
NBA2DPA |
|
NBA2LDBA |
|
NbaAdjMat<S> |
|
NbaDet |
This class provides a conversion from non-deterministic Büchi automata
into deterministic parity automata.
|
NbaDetArgs |
|
NbaDetArgs.Builder |
|
NbaDetConf<S> |
This is the structure containing all required information that is used in the
determinization process and is obtained based on an NbaDetArgs instance.
|
NbaDetConf.UpdateMode |
|
NbaDetConfSets |
these sets reflect the different determinisation components to be used in the DetState
i.e.
|
NbaDetState<S> |
This is the state type of the deterministic parity automaton produced by nbadet.
|
NbaLangInclusions |
This class glues available algorithms that can underapprox.
|
NbaLangInclusions.SimType |
Register new simulation algorithms here.
|
NbaSccInfo<S> |
This class wraps SccDecomposition, assigns each SCC an integer ID (in topological order)
and provides additional lookup tables to check various SCC properties and the SCC ID of states.
|
NbaSimAlgorithm<S,T> |
Interface that all pluggable language inclusion / simulation algorithms should implement.
|
Negation |
|
NonDeterministicConstructions |
|
NonDeterministicConstructions.CoSafety |
|
NonDeterministicConstructions.FgSafety |
|
NonDeterministicConstructions.GfCoSafety |
|
NonDeterministicConstructions.Safety |
|
NonDeterministicConstructions.Tracking |
|
NonDeterministicConstructionsPortfolio<A extends OmegaAcceptance> |
|
NormalForms |
|
Normalisation |
|
NullablePair<A,B> |
|
OinkGameSolver |
|
OinkGameSolver.OinkExecutionException |
Abstracts potential errors when executing oink to solve a game.
|
OmegaAcceptance |
|
OmegaAcceptanceCast |
This class provides functionality to cast an automaton to an automaton with a more generic
acceptance condition.
|
OutputWriters |
|
OutputWriters.AutomatonStats |
|
OutputWriters.ToHoa |
|
OwlModule<M extends OwlModule.Instance> |
|
OwlModule.AutomatonTransformer |
Derived transformer that casts the argument to an Automaton and optionally converts
the acceptance condition if possible.
|
OwlModule.Constructor<M> |
|
OwlModule.InputReader |
Input readers are tasked with providing input to the processing pipeline.
|
OwlModule.Instance |
|
OwlModule.LabelledFormulaTransformer |
|
OwlModule.OutputWriter |
The final piece of every pipeline, formatting the produced results and writing them on some
output.
|
OwlModule.Transformer |
Transformers are the central pieces of the pipeline concept.
|
OwlModuleRegistry |
A registry holding all modules used to parse the command line.
|
OwlModuleRegistry.OwlModuleNotFoundException |
|
OwlModuleRegistry.Type |
|
OwlParser |
|
OwlVersion |
|
OwlVersion.NameAndVersion |
|
Pair<A,B> |
|
ParityAcceptance |
|
ParityAcceptance.Parity |
|
ParityAcceptanceOptimizations |
|
ParityGameSolver |
|
ParityGameSolver.WinningRegions<S> |
|
ParityUtil |
|
PartialConfigurationParser |
Utility class used to parse a simplified command line (single exposed module with rest of the
pipeline preconfigured).
|
PartialModuleConfiguration |
|
Pebble<S> |
Abstraction of a single pebble in a multipebble simulation game.
|
Pipeline |
|
PipelineException |
|
PipelineParser |
|
PipelineParser.ModuleParseException |
|
Predicates |
|
PreprocessorVisitor |
|
PrintVisitor |
|
ProductState<T> |
|
ProductState |
|
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 |
|
RabinDegeneralization.DegeneralizedRabinState<S> |
|
RabinizerBuilder |
Central class handling the Rabinizer construction.
|
RabinizerConfiguration |
|
RabinizerState |
|
RankedSlice |
type/wrapper of ranked slices, which are just tuples of disjoint sets, with entries that are
additionally to the index order also ranked by some extra total order (i.e.
|
RankingState<S> |
|
Rewriter |
|
Rewriter.ToCoSafety |
|
Rewriter.ToSafety |
|
RobustLtlInputReader |
|
RobustLtlParser |
|
Robustness |
|
ROperator |
Weak Release.
|
RoundRobinState<E> |
|
RunUtil |
|
SccDecomposition<S> |
This class provides a decomposition into strongly connected components (SCCs) of a directed graph
given by either an Automaton or a SuccessorFunction .
|
Selector |
|
ServerCli |
|
SimplifierFactory |
|
SimplifierFactory.Mode |
|
SimplifierTransformer |
|
SimulationGame<S,T extends SimulationType.SimulationState<S>> |
Wrapper class that takes a simulationType and constructs the actual game itself based on the
state and transition function defined within the concrete simulationType.
|
SimulationStates |
|
SimulationStates.LookaheadSimulationState<S> |
|
SimulationStates.MultipebbleSimulationState<S> |
Holds all information necessary to implement forward multipebble simulations.
|
SimulationType<S,T extends SimulationType.SimulationState<S>> |
|
SimulationType.SimulationState<S> |
|
SimulationUtil |
|
SingletonAutomaton<S,A extends OmegaAcceptance> |
|
SmartSucc<S> |
This class acts like a "smart cache" for the states produced during NBA determinization.
|
Split |
|
SplitUntilVisitor |
|
State<T> |
|
Statistics |
|
StringUtil |
|
SuccessorFunction<S> |
|
SymmetricDRAConstruction<R extends GeneralizedRabinAcceptance> |
|
SymmetricEvaluatedFixpoints |
|
SymmetricEvaluatedFixpoints.DeterministicAutomata |
|
SymmetricEvaluatedFixpoints.NonDeterministicAutomata |
|
SymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance> |
|
SymmetricNBAConstruction<B extends GeneralizedBuchiAcceptance> |
|
SymmetricProductState |
|
SymmetricRankingState |
|
SymmetricRankingState |
|
SyntacticFragment |
|
SyntacticFragments |
|
SyntacticFragments.FormulaClass |
|
SyntacticFragments.Type |
|
SyntacticSimplifier |
|
Synthesis |
|
TokenErrorListener |
|
ToStateAcceptanceFixed |
Convert automaton to state-based acceptance.
|
Transition<S> |
|
TrieMap<K,V> |
A TrieMap is a Map with sequences as keys that are organized in a Trie for value retrieval.
|
TriFunction<A,B,C,R> |
|
TwoPartAutomaton<A,B,C extends OmegaAcceptance> |
|
UltimatelyPeriodicWord |
|
UnabbreviateVisitor |
|
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.Filter<S> |
|
Views.Filter.Builder<S> |
|
Visitor<R> |
|
WOperator |
Weak Until.
|
XDepthVisitor |
|
XOperator |
Next.
|
ZielonkaGameSolver |
|