Commit 9a2dbaee authored by Alexander Weigl's avatar Alexander Weigl
Browse files

Merge branch 'weigl/guirap' into 'master'

RunAllProofs in UI

This MR adds an action (under `file -> prove -> run all proofs`) in experimental mode
that allows an automatically running of a user- and pre-defined set of proofs in the UI.

These proofs are defined via file (each line is a proof-file) and can be given  via `export KEY_RUNALLPROOFS_UI_FILE=...`.


See merge request key/key!335
parents f80c0d24 e66f8986
......@@ -27,8 +27,9 @@ public final class Debug implements DebugMBean {
Boolean.valueOf(System.getProperty("KeyAssertionFlag", "true"));
/** has to be set in order to enable debugging */
public static boolean ENABLE_DEBUG = "on".equals(System
.getProperty("KeyDebugFlag"));
public static boolean ENABLE_DEBUG =
"on".equals(System.getProperty("KeyDebugFlag"))
|| "on".equals(System.getenv("KeyDebugFlag"));
/**
* Using the command line switch "-Dkey.debug.prefix" one can choose
......
......@@ -23,6 +23,7 @@ import de.uka.ilkd.key.control.TermLabelVisibilityManager;
import de.uka.ilkd.key.core.KeYMediator;
import de.uka.ilkd.key.core.KeYSelectionEvent;
import de.uka.ilkd.key.core.KeYSelectionListener;
import de.uka.ilkd.key.core.Main;
import de.uka.ilkd.key.gui.actions.*;
import de.uka.ilkd.key.gui.configuration.Config;
import de.uka.ilkd.key.gui.docking.DockingHelper;
......@@ -207,6 +208,8 @@ public final class MainWindow extends JFrame {
private LemmaGenerationAction loadUserDefinedTacletsForProvingAction;
private LemmaGenerationAction loadKeYTaclets;
private LemmaGenerationBatchModeAction lemmaGenerationBatchModeAction;
/**
* actions for changing the selection on the proof tree
*/
......@@ -748,7 +751,6 @@ public final class MainWindow extends JFrame {
fileMenu.add(quickLoadAction);
fileMenu.addSeparator();
fileMenu.add(proofManagementAction);
fileMenu.add(loadUserDefinedTacletsAction);
JMenu submenu = new JMenu("Prove");
fileMenu.add(submenu);
......@@ -756,6 +758,10 @@ public final class MainWindow extends JFrame {
submenu.add(loadUserDefinedTacletsForProvingAction);
submenu.add(loadKeYTaclets);
submenu.add(lemmaGenerationBatchModeAction);
if(Main.isExperimentalMode()) {
RunAllProofsAction runAllProofsAction = new RunAllProofsAction(this);
submenu.add(runAllProofsAction);
}
fileMenu.addSeparator();
fileMenu.add(recentFileMenu.getMenu());
fileMenu.addSeparator();
......
package de.uka.ilkd.key.gui.actions;
import de.uka.ilkd.key.core.KeYMediator;
import de.uka.ilkd.key.gui.ExampleChooser;
import de.uka.ilkd.key.gui.MainWindow;
import de.uka.ilkd.key.gui.WindowUserInterfaceControl;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.io.ProblemLoader;
import de.uka.ilkd.key.ui.MediatorProofControl;
import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
import java.awt.event.ActionEvent;
import java.io.*;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.Collectors;
/**
* This class provides an action for KeY UI which runs a set of specified proof files automatically.
* The intent of this class is to have a massive test feature for the quality assurance of the KeY during the
* release preparation.
*
* The used proofs can be given by the environment {@link #ENV_VARIABLE}.
* If this variable is not set, this class use the default {@code de/uka/ilkd/key/gui/actions/runallproofsui.txt}.
* See method {@link #loadFiles()} for more details.
*
* @author weigl
*/
public class RunAllProofsAction extends MainWindowAction {
public static final String ENV_VARIABLE = "KEY_RUNALLPROOFS_UI_FILE";
private static final @Nullable String RUN_ALL_PROOFS_UI = System.getenv(ENV_VARIABLE);
private static final String DEFAULT_FILE = "runallproofsui.txt";
private final File EXAMPLE_DIR = ExampleChooser.lookForExamples();
private List<File> files;
/**
* Loads the key file given in the file by environment variable {@link #ENV_VARIABLE}.
* If the content of {@link #ENV_VARIABLE} ({@link #RUN_ALL_PROOFS_UI}) is null,
* then {@link #DEFAULT_FILE} is used.
*/
private @NotNull List<File> loadFiles() throws IOException {
System.out.format("INFO: Use 'export %s=<...>' to set the input file for %s.\n",
ENV_VARIABLE, getClass().getSimpleName());
InputStream stream;
if (RUN_ALL_PROOFS_UI == null) {
stream = getClass().getResourceAsStream(DEFAULT_FILE);
} else {
stream = new FileInputStream(RUN_ALL_PROOFS_UI);
}
try (BufferedReader in = new BufferedReader(new InputStreamReader(stream))) {
return in.lines()
.filter(it -> !it.startsWith("#") && !it.trim().isEmpty())
.map(it -> (it.startsWith("/") ? new File(it) : new File(EXAMPLE_DIR, it)).getAbsoluteFile())
.collect(Collectors.toList());
}
}
public RunAllProofsAction(MainWindow mainWindow) {
super(mainWindow);
try {
files = loadFiles();
} catch (IOException e) {
files = new ArrayList<>();
e.printStackTrace();
}
setName("Run all proofs");
//setEnabled(Debug.ENABLE_DEBUG);
setTooltip("Open and run a pre-defined set of proofs for GUI testing. Enabled with KeY debug flag");
}
@Override
public void actionPerformed(ActionEvent e) {
WindowUserInterfaceControl ui = mainWindow.getUserInterface();
for (int i = 0; i < files.size(); i++) {
System.out.format("%2d: %s\n", i, files.get(i));
}
Runnable runnable = () -> {
for (File absFile : files) {
ui.reportStatus(this, "Run: " + absFile);
System.out.println("Run:" + absFile);
ProblemLoader problemLoader = ui.getProblemLoader(absFile, null, null, null, getMediator());
problemLoader.runSynchronously();
//mainWindow.loadProblem(absFile);
System.out.println("Loaded:" + absFile);
KeYMediator r = getMediator();
Proof proof = r.getSelectedProof();
MediatorProofControl control = ui.getProofControl();
if (control.isAutoModeSupported(proof)) {
control.startAutoMode(proof, proof.openEnabledGoals());
control.waitWhileAutoMode();
}
System.out.println("Finish: (" + getMediator().getSelectedProof().closed() + ") " + absFile);
getMediator().getSelectedProof().dispose();
}
System.out.println("==== RUN ALL PROOFS FINISHED ==== ");
};
Thread t = new Thread(runnable);
t.start();
/*
List<ExampleChooser.Example> examples = ExampleChooser.listExamples(exampleDir);
for (ExampleChooser.Example example : examples) {
File obl = example.getObligationFile();
mainWindow.loadProblem(obl);
}*/
}
}
# This file contains *.key files for be loaded with RunAllProofsAction
# in key.ui. You can use '#' for comments.
#
# Relative filenames are considered to be relative to the EXAMPLES_DIR.
# Absolute filenames are just absolute.
firstTouch/01-Agatha/project.key
firstTouch/02-Subset/project.key
firstTouch/05-ReverseArray/reverseArray.key
firstTouch/06-BinarySearch/project.key
firstTouch/07-Cell/project.key
firstTouch/08-Java5/project.key
firstTouch/09-Quicktour/project.key
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment