All Classes Interface Summary Class Summary Exception Summary
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> |
|
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> |
|
BoxNode<L,AP> |
Java representation of a "[]" (sub-)formula.
|
ColorVisualizationHelper |
|
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 |
|
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 M3CParser s.
|
FormulaNodeVisitor<T,L,AP> |
|
GfpNode<L,AP> |
Java representation of a "nu" (sub-)formula.
|
HTMLVisualizationHelper |
|
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 |
|
NNFVisitor<L,AP> |
A visitor that transforms a given mu-calculus or CTL formula to negation-normal-form.
|
NodeVisualizationHelper |
|
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> |
|
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 |
|
StringBDDSolver |
|
TransformerSerializer<T extends AbstractPropertyTransformer<T,L,AP>,L,AP> |
|
TrueNode<L,AP> |
Java representation of a "true" (sub-)formula.
|
TypedADDSolver<L,AP> |
|
TypedBDDSolver<L,AP> |
|
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 .
|