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 and Type | Field and Description |
---|---|
private SolverLauncher |
launcher |
private Proof |
originalProof |
private java.util.List<Proof> |
proofs |
private UserInterfaceControl |
ui |
Constructor and Description |
---|
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) |
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() |
private final UserInterfaceControl ui
private final Proof originalProof
private SolverLauncher launcher
private java.util.List<Proof> proofs
public 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)
private java.util.List<Proof> createProofsForTesting(boolean removeDuplicatePathConditions, boolean removePostCondition)
removeDuplicatePathConditions
- - if true no identical proofs will be createdremovePostCondition
- - if true, remove post conditionprivate void getNodesWithEmptyModalities(Node root, java.util.List<Node> nodes)
root
- the root nodenodes
- the nodes to be addedprivate Proof createProofForTesting_noDuplicate(Node node, java.util.List<Proof> otherProofs, boolean removePostCondition) throws ProofInputException
node
- the new root nodeotherProofs
- a list of proofs as described aboveremovePostCondition
- if true, then remove post conditionProofInputException
- exception for proof inputprotected Proof createProof(UserInterfaceControl ui, Proof oldProof, java.lang.String newName, Sequent newSequent) throws ProofInputException
ProofInputException
private boolean hasModalities(Term t, boolean checkUpdates)
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(SolverLauncher launcher, java.util.Collection<SMTSolver> problemSolvers, TestGenerationLog log, Proof originalProof) throws java.lang.Exception
java.lang.Exception
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.