de.uka.ilkd.key.smt.testgen

Class AbstractTestGenerator

java.lang.Object

de.uka.ilkd.key.smt.testgen.AbstractTestGenerator

Direct Known Subclasses:

TGWorker.MainWindowTestGenerator

public abstract class AbstractTestGenerator
extends java.lang.Object

Implementations of this class are used generate test cases or a given Proof.

This class provides the full logic independent from the a user interface. Subclasses are used to realize the user interface specific functionality.

Field Summary

Fields

Modifier and Type	Field and Description
private SolverLauncher	launcher
private Proof	originalProof
private java.util.List<Proof>	proofs
private UserInterfaceControl	ui

Constructor Summary

Constructors

Constructor and Description
AbstractTestGenerator(UserInterfaceControl ui, Proof originalProof) Constructor.

Method Summary

Modifier and Type	Method and Description
protected Proof	createProof(UserInterfaceControl ui, Proof oldProof, java.lang.String newName, Sequent newSequent)
private Proof	createProofForTesting_noDuplicate(Node node, java.util.List<Proof> otherProofs, boolean removePostCondition) Creates a proof with the specified node as its root.
private java.util.List<Proof>	createProofsForTesting(boolean removeDuplicatePathConditions, boolean removePostCondition) Creates a proof for each open node if the selected proof is open and a proof for each node on which the emptyModality rules was applied if the selected proof is closed.
void	dispose() Removes all generated proofs.
java.util.Collection<SMTSolver>	filterSolverResultsAndShowSolverStatistics(java.util.Collection<SMTSolver> problemSolvers, TestGenerationLog log)
protected void	generateFiles(SolverLauncher launcher, java.util.Collection<SMTSolver> problemSolvers, TestGenerationLog log, Proof originalProof)
void	generateTestCases(StopRequest stopRequest, TestGenerationLog log)
private void	getNodesWithEmptyModalities(Node root, java.util.List<Node> nodes) Adds all nodes on which the emptyModality rule was applied to the list.
protected Proof	getOriginalProof()
protected java.util.List<Proof>	getProofs()
protected UserInterfaceControl	getUI()
protected void	handleAllProofsPerformed(UserInterfaceControl ui)
protected void	handleLauncherStarted(java.util.Collection<SMTProblem> problems, java.util.Collection<SolverType> solverTypes, SolverLauncher launcher, TestGenerationLog log)
protected void	handleLauncherStopped(SolverLauncher launcher, java.util.Collection<SMTSolver> problemSolvers, TestGenerationLog log)
private boolean	hasModalities(Term t, boolean checkUpdates)
protected void	informAboutNoTestResults(SolverLauncher launcher, java.util.Collection<SMTSolver> problemSolvers, TestGenerationLog log, Proof originalProof) This method is used in the Eclipse world to show a dialog with the log.
static boolean	isSolverAvailable() Checks if the required SMT solver is available.
protected void	selectProof(UserInterfaceControl ui, Proof proof)
void	stopSMTLauncher()

Methods inherited from class java.lang.Object

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

Field Detail

ui

private final UserInterfaceControl ui

originalProof

private final Proof originalProof

launcher

private SolverLauncher launcher

proofs

private java.util.List<Proof> proofs

Constructor Detail

AbstractTestGenerator

public AbstractTestGenerator(UserInterfaceControl ui,
                             Proof originalProof)

Constructor.

Parameters:

ui - The UserInterfaceControl to use.

originalProof - The Proof to generate test cases for.

Method Detail

generateTestCases

public void generateTestCases(StopRequest stopRequest,
                              TestGenerationLog log)

handleAllProofsPerformed

protected void handleAllProofsPerformed(UserInterfaceControl ui)

dispose

public void dispose()

Removes all generated proofs.

selectProof

protected void selectProof(UserInterfaceControl ui,
                           Proof proof)

createProofsForTesting

private java.util.List<Proof> createProofsForTesting(boolean removeDuplicatePathConditions,
                                                     boolean removePostCondition)

Creates a proof for each open node if the selected proof is open and a proof for each node on which the emptyModality rules was applied if the selected proof is closed.

Parameters:

removeDuplicatePathConditions - - if true no identical proofs will be created

removePostCondition - - if true, remove post condition

Returns:

a list of proofs

getNodesWithEmptyModalities

private void getNodesWithEmptyModalities(Node root,
                                         java.util.List<Node> nodes)

Adds all nodes on which the emptyModality rule was applied to the list.

Parameters:

root - the root node

nodes - the nodes to be added

createProofForTesting_noDuplicate

private Proof createProofForTesting_noDuplicate(Node node,
                                                java.util.List<Proof> otherProofs,
                                                boolean removePostCondition)
                                         throws ProofInputException

Creates a proof with the specified node as its root. If an identical proof is found in otherProofs than null will be returned instead.

Parameters:

node - the new root node

otherProofs - a list of proofs as described above

removePostCondition - if true, then remove post condition

Returns:

the new proof with the specified root node

Throws:

ProofInputException - exception for proof input

createProof

protected Proof createProof(UserInterfaceControl ui,
                            Proof oldProof,
                            java.lang.String newName,
                            Sequent newSequent)
                     throws ProofInputException

Throws:

ProofInputException

hasModalities

private boolean hasModalities(Term t,
                              boolean checkUpdates)

handleLauncherStarted

protected void handleLauncherStarted(java.util.Collection<SMTProblem> problems,
                                     java.util.Collection<SolverType> solverTypes,
                                     SolverLauncher launcher,
                                     TestGenerationLog log)

handleLauncherStopped

protected void handleLauncherStopped(SolverLauncher launcher,
                                     java.util.Collection<SMTSolver> problemSolvers,
                                     TestGenerationLog log)

generateFiles

protected void generateFiles(SolverLauncher launcher,
                             java.util.Collection<SMTSolver> problemSolvers,
                             TestGenerationLog log,
                             Proof originalProof)
                      throws java.lang.Exception

Throws:

java.lang.Exception

informAboutNoTestResults

protected void informAboutNoTestResults(SolverLauncher launcher,
                                        java.util.Collection<SMTSolver> problemSolvers,
                                        TestGenerationLog log,
                                        Proof originalProof)

This method is used in the Eclipse world to show a dialog with the log.

filterSolverResultsAndShowSolverStatistics

public java.util.Collection<SMTSolver> filterSolverResultsAndShowSolverStatistics(java.util.Collection<SMTSolver> problemSolvers,
                                                                                  TestGenerationLog log)

stopSMTLauncher

public void stopSMTLauncher()

getOriginalProof

protected Proof getOriginalProof()

getProofs

protected java.util.List<Proof> getProofs()

getUI

protected UserInterfaceControl getUI()

isSolverAvailable

public static boolean isSolverAvailable()

Checks if the required SMT solver is available.

Returns:

true solver is available, false solver is not available.