Module net.automatalib.modelchecker.m3c

Package net.automatalib.modelchecker.m3c.solver

Class StringBDDSolver

java.lang.Object

net.automatalib.modelchecker.m3c.solver.BDDSolver<String,String>

net.automatalib.modelchecker.m3c.solver.StringBDDSolver

All Implemented Interfaces:

M3CSolver<String>, ModelChecker<String,ContextFreeModalProcessSystem<String,String>,FormulaNode<String,String>,WitnessTree<String,String>>

public class StringBDDSolver
extends BDDSolver<String,String>
implements M3CSolver<String>

A BDD solver for generic, string-based 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(String formula)	Checks whether the given formula is satisfied.
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

Method Detail

solve

public boolean solve(String formula)
              throws FormatException

Description copied from interface: M3CSolver

Checks whether the given formula is satisfied.

Specified by:

solve in interface M3CSolver<String>

Parameters:

formula - the formula whose satisfiability should be checked

Returns:

true if the formula is satisfied, false otherwise.

Throws:

FormatException - when the given formula object cannot be parsed

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)