Package net.automatalib.modelchecker.m3c.solver

Class BDDSolver<L,AP>

java.lang.Object

net.automatalib.modelchecker.m3c.solver.BDDSolver<L,AP>

Type Parameters:

L - edge label type

AP - atomic proposition type

All Implemented Interfaces:

ModelChecker<L,ContextFreeModalProcessSystem<L,AP>,FormulaNode<L,AP>,WitnessTree<L,AP>>

Direct Known Subclasses:

StringBDDSolver, TypedBDDSolver

public class BDDSolver<L,AP>
extends Object

Implementation based on property transformers being represented by BDDs (Binary Decision Diagrams).

Nested Class Summary

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelChecker

ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>

Constructor Summary

Constructors

Constructor	Description
BDDSolver(ContextFreeModalProcessSystem<L,AP> cfmps)

Method Summary

Modifier and Type	Method	Description
protected <TP extends ModalEdgeProperty> BDDTransformer<L,AP>	createInitTransformerEdge(DependencyGraph<L,AP> dependencyGraph, L edgeLabel, TP edgeProperty)
protected BDDTransformer<L,AP>	createInitTransformerEndNode(DependencyGraph<L,AP> dependencyGraph)
protected BDDTransformer<L,AP>	createInitTransformerNode(DependencyGraph<L,AP> dependencyGraph)
@Nullable WitnessTree<L,AP>	findCounterExample(ContextFreeModalProcessSystem<L,AP> cfmps, Collection<? extends L> inputs, FormulaNode<L,AP> formulaNode)	Try to find counter examples for the given property and automaton.
protected TransformerSerializer<BDDTransformer<L,AP>,L,AP>	getSerializer()
protected void	initDDManager(DependencyGraph<L,AP> dependencyGraph)
protected 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

Constructor Detail

BDDSolver

public BDDSolver(ContextFreeModalProcessSystem<L,AP> cfmps)

Method Detail

initDDManager

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

createInitTransformerEndNode

protected BDDTransformer<L,AP> createInitTransformerEndNode(DependencyGraph<L,AP> dependencyGraph)

createInitTransformerNode

protected BDDTransformer<L,AP> createInitTransformerNode(DependencyGraph<L,AP> dependencyGraph)

createInitTransformerEdge

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

shutdownDDManager

protected void shutdownDDManager()

getSerializer

protected TransformerSerializer<BDDTransformer<L,AP>,L,AP> getSerializer()

findCounterExample

public @Nullable WitnessTree<L,AP> findCounterExample(ContextFreeModalProcessSystem<L,AP> cfmps,
                                                            Collection<? extends L> inputs,
                                                            FormulaNode<L,AP> formulaNode)

Description copied from interface: ModelChecker

Try to find counter examples for the given property and automaton.

Specified by:

findCounterExample in interface ModelChecker<L,ContextFreeModalProcessSystem<L,AP>,FormulaNode<L,AP>,WitnessTree<L,AP>>

Parameters:

cfmps - the automaton to check the property on.

inputs - the alphabet.

formulaNode - the property.

Returns:

the counter examples, or null if no counter examples exist.

solve

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

solveAndRecordHistory

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