public abstract class AbstractTestGenerator
extends java.lang.Object
Proof
.
This class provides the full logic independent from the a user interface. Subclasses are used to realize the user interface specific functionality.
Modifier | Constructor and Description |
---|---|
protected |
AbstractTestGenerator(UserInterfaceControl ui,
Proof originalProof)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected Proof |
createProof(UserInterfaceControl ui,
Proof oldProof,
java.lang.String newName,
Sequent newSequent) |
void |
dispose()
Removes all generated proofs.
|
java.util.Collection<SMTSolver> |
filterSolverResultsAndShowSolverStatistics(java.util.Collection<SMTSolver> problemSolvers,
TestGenerationLog log) |
protected void |
generateFiles(java.util.Collection<SMTSolver> problemSolvers,
TestGenerationLog log,
Proof originalProof) |
void |
generateTestCases(StopRequest stopRequest,
TestGenerationLog log) |
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) |
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() |
protected AbstractTestGenerator(UserInterfaceControl ui, Proof originalProof)
ui
- The UserInterfaceControl
to use.originalProof
- The Proof
to generate test cases for.public void generateTestCases(StopRequest stopRequest, TestGenerationLog log)
protected void handleAllProofsPerformed(UserInterfaceControl ui)
public void dispose()
protected void selectProof(UserInterfaceControl ui, Proof proof)
protected Proof createProof(UserInterfaceControl ui, Proof oldProof, java.lang.String newName, Sequent newSequent) throws ProofInputException
ProofInputException
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)
protected void generateFiles(java.util.Collection<SMTSolver> problemSolvers, TestGenerationLog log, Proof originalProof) throws java.io.IOException
java.io.IOException
protected void informAboutNoTestResults(SolverLauncher launcher, java.util.Collection<SMTSolver> problemSolvers, TestGenerationLog log, Proof originalProof)
public java.util.Collection<SMTSolver> filterSolverResultsAndShowSolverStatistics(java.util.Collection<SMTSolver> problemSolvers, TestGenerationLog log)
public void stopSMTLauncher()
protected Proof getOriginalProof()
protected java.util.List<Proof> getProofs()
protected UserInterfaceControl getUI()
public static boolean isSolverAvailable()
true
solver is available, false
solver is not available.Copyright © 2003-2019 The KeY-Project.