Module net.automatalib.modelchecker.m3c

Package net.automatalib.modelchecker.m3c.solver

Class AbstractDDSolver<T extends AbstractPropertyTransformer<T,L,AP>,L,AP>

java.lang.Object

net.automatalib.modelchecker.m3c.solver.AbstractDDSolver<T,L,AP>

Type Parameters:

T - property transformer type

L - edge label type

AP - atomic proposition type

Direct Known Subclasses:

ADDSolver, BDDSolver

public abstract class AbstractDDSolver<T extends AbstractPropertyTransformer<T,L,AP>,L,AP>
extends Object

Base implementation of the model checker which supports different types of property transformers.

Method Summary

Modifier and Type	Method	Description
protected abstract <TP extends ModalEdgeProperty> T	createInitTransformerEdge(DependencyGraph<L,AP> dependencyGraph, L edgeLabel, TP edgeProperty)
protected abstract T	createInitTransformerEndNode(DependencyGraph<L,AP> dependencyGraph)
protected abstract T	createInitTransformerNode(DependencyGraph<L,AP> dependencyGraph)
@Nullable WitnessTree<L,AP>	findWitness(FormulaNode<L,AP> formulaNode)
protected abstract TransformerSerializer<T,L,AP>	getSerializer()
protected abstract void	initDDManager(DependencyGraph<L,AP> dependencyGraph)
protected abstract void	shutdownDDManager()
boolean	solve(FormulaNode<L,AP> formula)
SolverHistory<T,L,AP>	solveAndRecordHistory(FormulaNode<L,AP> formula)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Details

findWitness

public @Nullable WitnessTree<L,AP> findWitness(FormulaNode<L,AP> formulaNode)

solve

public boolean solve(FormulaNode<L,AP> formula)

solveAndRecordHistory

public SolverHistory<T,L,AP> solveAndRecordHistory(FormulaNode<L,AP> formula)

initDDManager

protected abstract void initDDManager(DependencyGraph<L,AP> dependencyGraph)

createInitTransformerEdge

protected abstract <TP extends ModalEdgeProperty> T createInitTransformerEdge(DependencyGraph<L,AP> dependencyGraph,
 L edgeLabel,
 TP edgeProperty)

createInitTransformerEndNode

protected abstract T createInitTransformerEndNode(DependencyGraph<L,AP> dependencyGraph)

createInitTransformerNode

protected abstract T createInitTransformerNode(DependencyGraph<L,AP> dependencyGraph)

shutdownDDManager

protected abstract void shutdownDDManager()

getSerializer

protected abstract TransformerSerializer<T,L,AP> getSerializer()