Package net.automatalib.modelchecker.m3c.solver

Interface Summary

Interface	Description
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.

Class Summary

Class	Description
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	A factory for constructing M3CSolvers depending on the given ContextFreeModalProcessSystem.
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.
TypedADDSolver<L,AP>	An ADD solver for strongly-typed formulas.
TypedBDDSolver<L,AP>	A BDD solver for strongly-typed formulas.
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.