All Classes

Class	Description
AbstractBinaryFormulaNode<L,AP>	Abstract super-class for binary (sub-) formulas.
AbstractFixedPointFormulaNode<L,AP>	Abstract super-class for fix-point (sub-) formulas.
AbstractFormulaNode<L,AP>	Abstract super-class for (sub-) formulas.
AbstractModalFormulaNode<L,AP>	Abstract super-class for modal (sub-) formulas.
AbstractPropertyTransformer<T extends AbstractPropertyTransformer<T,L,AP>,L,AP>	Base class used to represent a property transformer, i.e., a function which maps a subset of formulas to a subset of formulas.
AbstractUnaryFormulaNode<L,AP>	Abstract super-class for unary (sub-) formulas.
ADDSolver<L,AP>	Implementation based on property transformers being represented by ADDs (Algebraic Decision Diagrams).
ADDTransformer<L,AP>	An ADDTransformer represents a property transformer for a single ADD (Algebraic Decision Diagram).
ADDTransformerSerializer<L,AP>	This class can be used to serialize and deserialize ADDTransformers.
AFNode<L,AP>	Java representation of a "AF" (sub-)formula.
AGNode<L,AP>	Java representation of a "AG" (sub-)formula.
AndNode<L,AP>	Java representation of a "&&" (sub-)formula.
AtomicNode<L,AP>	Java representation of an "atomic proposition" (sub-)formula.
AUNode<L,AP>	Java representation of a "AU" (sub-)formula.
AWUNode<L,AP>	Java representation of an "AWU" (sub-)formula.
BDDSolver<L,AP>	Implementation based on property transformers being represented by BDDs (Binary Decision Diagrams).
BDDTransformer<L,AP>	A BDDTransformer represents a property transformer for a list of BDDs (Binary Decision Diagrams), one per subformula.
BDDTransformerSerializer<L,AP>	This class can be used to serialize and deserialize BDDTransformers.
BoxNode<L,AP>	Java representation of a "[]" (sub-)formula.
ColorVisualizationHelper	A VisualizationHelper for WitnessTrees that emphasizes nodes and edges of the witness and de-emphasizes the remaining ones.
CTLToMuCalc<L,AP>	A visitor that transforms a given CTL formula to an equivalent mu-calculus formula.
DependencyGraph<L,AP>	A dependency graph is used to represent a hierarchical equational system.
DiamondNode<L,AP>	Java representation of a "<>" (sub-)formula.
DiamondOperation<AP>	Implementation of the diamond function.
DiamondOperationDeadlock<AP>	Implementation of the diamond function when the node has exactly one successor.
EdgeVisualizationHelper	A VisualizationHelper for WitnessTrees that emphasizes edges of the witness and de-emphasizes the remaining ones.
EFNode<L,AP>	Java representation of a "EF" (sub-)formula.
EGNode<L,AP>	Java representation of a "EG" (sub-)formula.
EquationalBlock<L,AP>	Represents an equational block that aggregates its reference formula nodes.
EUNode<L,AP>	Java representation of a "EU" (sub-)formula.
EWUNode<L,AP>	Java representation of a "EWU" (sub-)formula.
FalseNode<L,AP>	Java representation of a "false" (sub-)formula.
FormulaNode<L,AP>	Generic interface for formulas return by M3CParsers.
FormulaNodeVisitor<T,L,AP>
GfpNode<L,AP>	Java representation of a "nu" (sub-)formula.
HTMLVisualizationHelper	A VisualizationHelper for WitnessTrees that renders the node labels as an HTML-based table.
LfpNode<L,AP>	Java representation of a "mu" (sub-)formula.
M3CParser	This class can be used to parse formulas in CTL and the mu-calculus.
M3CSolver<F>	An interface for a generic M3C solver which may need to parse the given formula and thus may throw an exception when doing so.
M3CSolver.TypedM3CSolver<F>	A specialized M3CSolver which no longer throws a ParseException when solving a formula, but requires a type-safe formula object.
M3CSolvers	A factory for constructing M3CSolvers depending on the given ContextFreeModalProcessSystem.
NNFVisitor<L,AP>	A visitor that transforms a given mu-calculus or CTL formula to negation-normal-form.
NodeVisualizationHelper	A VisualizationHelper for WitnessTrees that emphasizes nodes of the witness and de-emphasizes the remaining ones.
NotNode<L,AP>	Java representation of a "!"
OrNode<L,AP>	Java representation of a "||" (sub-)formula.
ParseException	This exception is thrown when parse errors are encountered.
SolverData<N,T extends AbstractPropertyTransformer<T,L,AP>,L,AP>	A class used to store ProceduralModalProcessGraph-specific data for the SolverHistory.
SolverHistory<T extends AbstractPropertyTransformer<T,L,AP>,L,AP>	A class used to store internal information produced by AbstractDDSolver.solveAndRecordHistory(net.automatalib.modelchecker.m3c.formula.FormulaNode<L, AP>) while checking the satisfiability of a formula.
SolverState<N,T extends AbstractPropertyTransformer<T,L,AP>,L,AP>	Stores internal information produced during the update of a node in AbstractDDSolver.
StringADDSolver	An ADD solver for generic, string-based formulas.
StringBDDSolver	A BDD solver for generic, string-based formulas.
TransformerSerializer<T extends AbstractPropertyTransformer<T,L,AP>,L,AP>	Utility interface for serializing AbstractPropertyTransformer implementations.
TrueNode<L,AP>	Java representation of a "true" (sub-)formula.
TypedADDSolver<L,AP>	An ADD solver for strongly-typed formulas.
TypedBDDSolver<L,AP>	A BDD solver for strongly-typed formulas.
VariableNode<L,AP>	Java representation of an "X" (sub-)formula.
WitnessTree<L,AP>	A tree-like Graph that represents the BFS-style exploration of the tableau generated by the WitnessTreeExtractor.
WitnessTreeState<N,L,E,AP>	A utility class that represents a current configuration (node property) in the WitnessTree.