public abstract class AbstractTestGenerator extends 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 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,
String newName,
Sequent newSequent) |
private Proof |
createProofForTesting_noDuplicate(Node node,
List<Proof> otherProofs,
boolean removePostCondition)
Creates a proof with the specified node as its root.
|
private 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.
|
Collection<SMTSolver> |
filterSolverResultsAndShowSolverStatistics(Collection<SMTSolver> problemSolvers,
TestGenerationLog log) |
protected void |
generateFiles(SolverLauncher launcher,
Collection<SMTSolver> problemSolvers,
TestGenerationLog log,
Proof originalProof) |
void |
generateTestCases(StopRequest stopRequest,
TestGenerationLog log) |
private void |
getNodesWithEmptyModalities(Node root,
List<Node> nodes)
Adds all nodes on which the emptyModality rule was applied to the list.
|
protected Proof |
getOriginalProof() |
protected List<Proof> |
getProofs() |
protected UserInterfaceControl |
getUI() |
protected void |
handleAllProofsPerformed(UserInterfaceControl ui) |
protected void |
handleLauncherStarted(Collection<SMTProblem> problems,
Collection<SolverType> solverTypes,
SolverLauncher launcher,
TestGenerationLog log) |
protected void |
handleLauncherStopped(SolverLauncher launcher,
Collection<SMTSolver> problemSolvers,
TestGenerationLog log) |
private boolean |
hasModalities(Term t,
boolean checkUpdates) |
protected void |
informAboutNoTestResults(SolverLauncher launcher,
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
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 List<Proof> createProofsForTesting(boolean removeDuplicatePathConditions, boolean removePostCondition)
mediator
- removeDuplicatePathConditions
- - if true no identical proofs will be createdprivate void getNodesWithEmptyModalities(Node root, List<Node> nodes)
root
- nodes
- private Proof createProofForTesting_noDuplicate(Node node, List<Proof> otherProofs, boolean removePostCondition) throws ProofInputException
node
- otherProofs
- removePostCondition
- TODOProofInputException
protected Proof createProof(UserInterfaceControl ui, Proof oldProof, String newName, Sequent newSequent) throws ProofInputException
ProofInputException
private boolean hasModalities(Term t, boolean checkUpdates)
protected void handleLauncherStarted(Collection<SMTProblem> problems, Collection<SolverType> solverTypes, SolverLauncher launcher, TestGenerationLog log)
protected void handleLauncherStopped(SolverLauncher launcher, Collection<SMTSolver> problemSolvers, TestGenerationLog log)
protected void generateFiles(SolverLauncher launcher, Collection<SMTSolver> problemSolvers, TestGenerationLog log, Proof originalProof) throws Exception
Exception
protected void informAboutNoTestResults(SolverLauncher launcher, Collection<SMTSolver> problemSolvers, TestGenerationLog log, Proof originalProof)
public Collection<SMTSolver> filterSolverResultsAndShowSolverStatistics(Collection<SMTSolver> problemSolvers, TestGenerationLog log)
public void stopSMTLauncher()
protected Proof getOriginalProof()
protected UserInterfaceControl getUI()
public static boolean isSolverAvailable()
true
solver is available, false
solver is not available.