de.uka.ilkd.key.gui.actions

Class CounterExampleAction.MainWindowCounterExampleGenerator

java.lang.Object

de.uka.ilkd.key.smt.counterexample.AbstractCounterExampleGenerator

de.uka.ilkd.key.gui.actions.CounterExampleAction.MainWindowCounterExampleGenerator

Enclosing class:

CounterExampleAction

public static class CounterExampleAction.MainWindowCounterExampleGenerator
extends AbstractCounterExampleGenerator

Performs the 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.

Field Summary

Fields

Modifier and Type	Field and Description
private KeYMediator	mediator The KeYMediator to use.

Constructor Summary

Constructors

Constructor and Description
MainWindowCounterExampleGenerator(KeYMediator mediator) Constructor.

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.smt.counterexample.AbstractCounterExampleGenerator

createNewSequent, isSolverAvailable, searchCounterExample

Methods inherited from class java.lang.Object

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

Field Detail

mediator

private final KeYMediator mediator

The KeYMediator to use.

Constructor Detail

MainWindowCounterExampleGenerator

public MainWindowCounterExampleGenerator(KeYMediator mediator)

Constructor.

Parameters:

mediator - The KeYMediator to use.

Method Detail

createProof

protected Proof createProof(UserInterfaceControl ui,
                            Proof oldProof,
                            Sequent oldSequent,
                            java.lang.String proofName)

Creates a new Proof.

Specified by:

createProof in class AbstractCounterExampleGenerator

Parameters:

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.

Returns:

The created Proof.

semanticsBlastingCompleted

protected void semanticsBlastingCompleted(UserInterfaceControl ui)

This method is called after the SemanticsBlastingMacro has been executed.

Overrides:

semanticsBlastingCompleted in class AbstractCounterExampleGenerator

Parameters:

ui - The UserInterfaceControl to use.

createSolverListener

protected SolverLauncherListener createSolverListener(SMTSettings settings,
                                                      Proof proof)

Creates the SolverLauncherListener which handles the results of the launched SMT solver.

Specified by:

createSolverListener in class AbstractCounterExampleGenerator

Parameters:

settings - The SMTSettings.

proof - The Proof on which the SMT solver will be performed.

Returns:

The SolverLauncherListener to use.