Package net.automatalib.modelchecker.m3c.solver

Class StringADDSolver

java.lang.Object

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

net.automatalib.modelchecker.m3c.solver.StringADDSolver

All Implemented Interfaces:

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

public class StringADDSolver
extends ADDSolver<String,String>
implements M3CSolver<String>

An ADD 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.ADDSolver

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 ParseException

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:

ParseException - 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)