public static class CounterExampleAction.MainWindowCounterExampleGenerator extends AbstractCounterExampleGenerator
SemanticsBlastingMacro
in a Proof
registered
in the MainWindow
and thus visible to the user.
Results are shown with help of the SolverListener
.
This class provides only the user interface and no counter example
generation logic which is implemented by the
AbstractCounterExampleGenerator
.
Modifier and Type | Field and Description |
---|---|
private KeYMediator |
mediator
The
KeYMediator to use. |
Constructor and Description |
---|
MainWindowCounterExampleGenerator(KeYMediator mediator)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected Proof |
createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
protected SolverLauncherListener |
createSolverListener(SMTSettings settings,
Proof proof)
Creates the
SolverLauncherListener which handles the results
of the launched SMT solver. |
protected void |
semanticsBlastingCompleted(UserInterfaceControl ui)
This method is called after the
SemanticsBlastingMacro has been executed. |
createNewSequent, isSolverAvailable, searchCounterExample
private final KeYMediator mediator
KeYMediator
to use.public MainWindowCounterExampleGenerator(KeYMediator mediator)
mediator
- The KeYMediator
to use.protected Proof createProof(UserInterfaceControl ui, Proof oldProof, Sequent oldSequent, java.lang.String proofName)
Proof
.createProof
in class AbstractCounterExampleGenerator
ui
- The UserInterfaceControl
to use.oldProof
- The old Proof
used as template to instantiate a new one.oldSequent
- The Sequent
to find a counter example for.proofName
- The name for the new proof.Proof
.protected void semanticsBlastingCompleted(UserInterfaceControl ui)
SemanticsBlastingMacro
has been executed.semanticsBlastingCompleted
in class AbstractCounterExampleGenerator
ui
- The UserInterfaceControl
to use.protected SolverLauncherListener createSolverListener(SMTSettings settings, Proof proof)
SolverLauncherListener
which handles the results
of the launched SMT solver.createSolverListener
in class AbstractCounterExampleGenerator
settings
- The SMTSettings
.proof
- The Proof
on which the SMT solver will be performed.SolverLauncherListener
to use.