Package net.automatalib.modelchecker.m3c.solver

Class TypedBDDSolver<L,AP>

java.lang.Object

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

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

Type Parameters:

L - label type

AP - atomic proposition type

All Implemented Interfaces:

M3CSolver<FormulaNode<L,AP>>, M3CSolver.TypedM3CSolver<FormulaNode<L,AP>>, ModelChecker<L,ContextFreeModalProcessSystem<L,AP>,FormulaNode<L,AP>,WitnessTree<L,AP>>

public class TypedBDDSolver<L,AP>
extends BDDSolver<L,AP>
implements M3CSolver.TypedM3CSolver<FormulaNode<L,AP>>

A BDD solver for strongly-typed formulas.

Nested Class Summary

Nested classes/interfaces inherited from interface net.automatalib.modelchecker.m3c.solver.M3CSolver

M3CSolver.TypedM3CSolver<F>

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

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

Method Summary

Modifier and Type	Method	Description
@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.
boolean	solve(FormulaNode<L,AP> formula)
SolverHistory<T,L,AP>	solveAndRecordHistory(FormulaNode<L,AP> formula)

Methods inherited from class net.automatalib.modelchecker.m3c.solver.BDDSolver

createInitTransformerEdge, createInitTransformerEndNode, createInitTransformerNode, getSerializer, initDDManager, shutdownDDManager

Methods inherited from class java.lang.Object

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

Methods inherited from interface net.automatalib.modelchecker.m3c.solver.M3CSolver.TypedM3CSolver

solve

Method Detail

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)