Package net.automatalib.modelchecker.m3c.solver

Class M3CSolvers

java.lang.Object

net.automatalib.modelchecker.m3c.solver.M3CSolvers

public final class M3CSolvers
extends Object

A factory for constructing M3CSolvers depending on the given ContextFreeModalProcessSystem.

Method Summary

Modifier and Type	Method	Description
static M3CSolver<String>	addSolver(ContextFreeModalProcessSystem<String,String> cfmps)	Returns an ADD-backed M3CSolver solver for string-based modal context-free process systems.
static M3CSolver<String>	bddSolver(ContextFreeModalProcessSystem<String,String> cfmps)	Returns a BDD-backed M3CSolver solver for string-based ContextFreeModalProcessSystem.
static M3CSolver<String>	solver(ContextFreeModalProcessSystem<String,String> cfmps)	Returns a default M3CSolver solver for string-based modal context-free process systems.
static <L,AP> M3CSolver.TypedM3CSolver<FormulaNode<L,AP>>	typedADDSolver(ContextFreeModalProcessSystem<L,AP> cfmps)	Returns an ADD-backed M3CSolver.TypedM3CSolver solver for strongly-typed modal context-free process systems.
static <L,AP> M3CSolver.TypedM3CSolver<FormulaNode<L,AP>>	typedBDDSolver(ContextFreeModalProcessSystem<L,AP> cfmps)	Returns a BDD-backed M3CSolver.TypedM3CSolver solver for strongly-typed ContextFreeModalProcessSystem.
static <L,AP> M3CSolver.TypedM3CSolver<FormulaNode<L,AP>>	typedSolver(ContextFreeModalProcessSystem<L,AP> cfmps)	Returns a default M3CSolver.TypedM3CSolver solver for strongly-typed modal context-free process systems.

Methods inherited from class java.lang.Object

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

Method Detail

solver

public static M3CSolver<String> solver(ContextFreeModalProcessSystem<String,String> cfmps)

Returns a default M3CSolver solver for string-based modal context-free process systems. This method currently delegates solver construction to bddSolver(ContextFreeModalProcessSystem).

Parameters:

cfmps - the system to evaluate formulas on

Returns:

a default M3CSolver solver for string-based modal context-free process systems

See Also:

bddSolver(ContextFreeModalProcessSystem)

typedSolver

public static <L,AP> M3CSolver.TypedM3CSolver<FormulaNode<L,AP>> typedSolver(ContextFreeModalProcessSystem<L,AP> cfmps)

Returns a default M3CSolver.TypedM3CSolver solver for strongly-typed modal context-free process systems. This method currently delegates solver construction to typedBDDSolver(ContextFreeModalProcessSystem).

Type Parameters:

L - label type

AP - atomic proposition type

Parameters:

cfmps - the system to evaluate formulas on

Returns:

a default M3CSolver.TypedM3CSolver solver for strongly-typed modal context-free process systems

See Also:

typedBDDSolver(ContextFreeModalProcessSystem)

addSolver

public static M3CSolver<String> addSolver(ContextFreeModalProcessSystem<String,String> cfmps)

Returns an ADD-backed M3CSolver solver for string-based modal context-free process systems.

Parameters:

cfmps - the system to evaluate formulas on

Returns:

an ADD-backed M3CSolver solver for string-based modal context-free process systems

typedADDSolver

public static <L,AP> M3CSolver.TypedM3CSolver<FormulaNode<L,AP>> typedADDSolver(ContextFreeModalProcessSystem<L,AP> cfmps)

Returns an ADD-backed M3CSolver.TypedM3CSolver solver for strongly-typed modal context-free process systems.

Type Parameters:

L - label type

AP - atomic proposition type

Parameters:

cfmps - the system to evaluate formulas on

Returns:

an ADD-backed M3CSolver.TypedM3CSolver solver for strongly-typed modal context-free process systems

bddSolver

public static M3CSolver<String> bddSolver(ContextFreeModalProcessSystem<String,String> cfmps)

Returns a BDD-backed M3CSolver solver for string-based ContextFreeModalProcessSystem.

Parameters:

cfmps - the system to evaluate formulas on

Returns:

an ADD-backed M3CSolver for string-based systems

typedBDDSolver

public static <L,AP> M3CSolver.TypedM3CSolver<FormulaNode<L,AP>> typedBDDSolver(ContextFreeModalProcessSystem<L,AP> cfmps)

Returns a BDD-backed M3CSolver.TypedM3CSolver solver for strongly-typed ContextFreeModalProcessSystem.

Type Parameters:

L - label type

AP - atomic proposition type

Parameters:

cfmps - the system to evaluate formulas on

Returns:

a BDD-backed M3CSolver.TypedM3CSolver for strongly-typed systems