ADDSolver<L,AP> 
Implementation based on property transformers being represented by ADDs (Algebraic Decision Diagrams).

BDDSolver<L,AP> 
Implementation based on property transformers being represented by BDDs (Binary Decision Diagrams).

M3CSolvers 

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 

TypedADDSolver<L,AP> 

TypedBDDSolver<L,AP> 

WitnessTree<L,AP> 
A treelike Graph that represents the BFSstyle 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 .
