Commit 2dc8e935 authored by Sarah Grebing's avatar Sarah Grebing

First Prototype with GUI (atm w.o. threading; will be insrted in next commit)

parent 0c1e07d3
Pipeline #10798 failed with stage
in 1 minute and 18 seconds
......@@ -115,10 +115,29 @@
<visitor>true</visitor>
</configuration>
</plugin>
<plugin>
<groupId>com.zenjava</groupId>
<artifactId>javafx-maven-plugin</artifactId>
<version>2.0</version>
</plugin>
<plugin>
<groupId>com.zenjava</groupId>
<artifactId>javafx-maven-plugin</artifactId>
<version>2.0</version>
<configuration>
<mainClass>ProofScriptDebugger.Main</mainClass>
</configuration>
</plugin>
</plugins>
</build>
<dependencies>
<dependency>
<groupId>org.fxmisc.richtext</groupId>
<artifactId>richtextfx</artifactId>
<version>0.6.10</version>
</dependency>
<dependency>
<groupId>junit</groupId>
<artifactId>junit</artifactId>
......@@ -185,7 +204,11 @@
<artifactId>commons-cli</artifactId>
<version>1.4</version>
</dependency>
<dependency>
<groupId>com.google.guava</groupId>
<artifactId>guava</artifactId>
<version>22.0</version>
</dependency>
</dependencies>
......
package edu.kit.formal.gui;
import java.io.*;
/**
* Created by sarah on 5/29/17.
*/
public class FileUtils {
public static BufferedReader readFile(File file) {
BufferedReader br = null;
try {
br = new BufferedReader(new FileReader(file));
StringBuilder sb = new StringBuilder();
String line = br.readLine();
while (line != null) {
sb.append(line);
sb.append(System.lineSeparator());
line = br.readLine();
}
} catch (FileNotFoundException e) {
e.printStackTrace();
} catch (IOException e) {
e.printStackTrace();
}
return br;
}
}
package edu.kit.formal.gui;/**
* Created by sarah on 5/26/17.
*/
import edu.kit.formal.gui.controller.RootController;
import edu.kit.formal.gui.model.RootModel;
import javafx.application.Application;
import javafx.fxml.FXMLLoader;
import javafx.scene.Parent;
import javafx.scene.Scene;
import javafx.stage.Stage;
import java.io.IOException;
public class ProofScriptDebugger extends Application {
public static void main(String[] args) {
launch(args);
}
@Override
public void start(Stage primaryStage) {
RootModel rm = new RootModel();
FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/DebuggerMain.fxml"));
Parent root = null;
try {
root = (Parent) fxmlLoader.load();
RootController controller = fxmlLoader.<RootController>getController();
controller.setStage(primaryStage);
controller.setModel(rm);
controller.init();
Scene scene = new Scene(root);
primaryStage.setTitle("Proof Script Debugger");
primaryStage.setScene(scene);
primaryStage.show();
} catch (IOException e) {
e.printStackTrace();
}
}
}
package edu.kit.formal.gui.controller;
import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import javafx.fxml.FXML;
import javafx.fxml.FXMLLoader;
import javafx.scene.control.ListCell;
import javafx.scene.control.ListView;
import javafx.scene.control.TextArea;
import javafx.scene.layout.VBox;
import java.io.IOException;
/**
* Created by sarah on 5/27/17.
*/
public class ListGoalView extends VBox {
@FXML
private ListView<GoalNode<KeyData>> listOfGoals;
@FXML
private TextArea goalNodeView;
private RootModel rootModel;
public ListGoalView() {
FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/GoalView.fxml"));
fxmlLoader.setRoot(this);
fxmlLoader.setController(this);
try {
fxmlLoader.load();
} catch (IOException exception) {
throw new RuntimeException(exception);
}
listOfGoals.setCellFactory(list -> new GoalNodeCell());
}
public void setRootModel(RootModel rootModel) {
this.rootModel = rootModel;
}
public void init() {
this.listOfGoals.itemsProperty().bind(this.rootModel.currentGoalNodesProperty());
// this.listOfGoals.itemsProperty().bind(this.rootModel.currentGoalNodesProperty());
goalNodeView.textProperty().bind(listOfGoals.getSelectionModel().selectedItemProperty().asString());
}
private static class GoalNodeCell extends ListCell<GoalNode<KeyData>> {
@Override
protected void updateItem(GoalNode<KeyData> item, boolean empty) {
super.updateItem(item, empty);
if (item != null) {
setText(item.toListLabelForKeYData());
}
}
}
}
package edu.kit.formal.gui.controller;
import edu.kit.formal.gui.FileUtils;
import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.Interpreter;
import edu.kit.formal.interpreter.KeYInterpreterFacade;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.interpreter.dbg.Debugger;
import javafx.fxml.FXML;
import javafx.fxml.Initializable;
import javafx.scene.control.*;
import javafx.scene.layout.Pane;
import javafx.stage.FileChooser;
import javafx.stage.Stage;
import lombok.Setter;
import java.io.File;
import java.net.URL;
import java.util.List;
import java.util.ResourceBundle;
/**
* Created by sarah on 5/26/17.
*/
public class RootController implements Initializable {
@FXML
Pane rootPane;
@FXML
SplitPane splitPane;
@FXML
ScrollPane scrollPaneCode;
/***********************************************************************************************************
* Code Area
* **********************************************************************************************************/
@FXML
ScriptArea scriptArea;
/***********************************************************************************************************
* MenuBar
* **********************************************************************************************************/
@FXML
MenuBar menubar;
@FXML
Menu fileMenu;
@FXML
MenuItem closeMenuItem;
/***********************************************************************************************************
* ToolBar
* **********************************************************************************************************/
@FXML
ToolBar toolbar;
@FXML
Button buttonStartInterpreter;
@FXML
Button startDebugMode;
/***********************************************************************************************************
* GoalView
* **********************************************************************************************************/
@FXML
ListGoalView goalView;
private RootModel model;
@Setter
private Interpreter<KeyData> interpreter;
@Setter
private Debugger debugger;
private Stage stage;
@FXML
public void executeScript() {
buttonStartInterpreter.setText("Interpreting...");
startDebugMode.setDisable(true);
String currentScript = this.model.getCurrentScript();
KeYInterpreterFacade inter = new KeYInterpreterFacade();
State<KeyData> s = inter.executeScriptWithKeYProblemFile(this.model.getCurrentScript(), this.model.getKeYFile());
List<GoalNode<KeyData>> g = s.getGoals();
this.model.getCurrentGoalNodes().addAll(g);
buttonStartInterpreter.setText("execute Script");
}
@FXML
public void changeToDebugMode() {
}
@FXML
protected void closeProgram() {
System.exit(0);
}
@FXML
protected void openScript() {
File scriptFile = openFileChooserDialog("Select Script File", "Proof Script File", "kps");
if (scriptFile != null) {
model.setScriptFile(scriptFile);
this.model.currentScriptProperty().set(FileUtils.readFile(scriptFile).toString());
}
}
@FXML
protected void loadKeYFile() {
File keyFile = openFileChooserDialog("Select KeY File", "KeY Files", "key", "java", "script");
this.model.setKeYFile(keyFile);
}
public void setStage(Stage stage) {
this.stage = stage;
}
/**
* @param title
* @param description
* @param fileEndings
* @return
*/
private File openFileChooserDialog(String title, String description, String... fileEndings) {
FileChooser fileChooser = new FileChooser();
fileChooser.setTitle(title);
fileChooser.setSelectedExtensionFilter(new FileChooser.ExtensionFilter(description, fileEndings));
fileChooser.setInitialDirectory(new File("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/interpreter/contraposition/"));
File file = fileChooser.showOpenDialog(this.stage);
return file;
}
public void setModel(RootModel model) {
this.model = model;
}
public void init() {
scriptArea.setRootModel(this.model);
scriptArea.init();
goalView.setRootModel(this.model);
goalView.init();
}
@Override
public void initialize(URL location, ResourceBundle resources) {
}
}
package edu.kit.formal.gui.controller;
import edu.kit.formal.gui.model.RootModel;
import javafx.beans.property.SimpleObjectProperty;
import javafx.beans.value.ObservableValue;
import lombok.Getter;
import org.fxmisc.richtext.CodeArea;
import org.fxmisc.richtext.LineNumberFactory;
/**
* Created by sarah on 5/27/17.
*/
public class ScriptArea extends CodeArea {
@Getter
private RootModel rootModel;
public void setRootModel(RootModel rootModel) {
this.rootModel = rootModel;
ObservableValue<String> stringObservableValue = this.textProperty();
SimpleObjectProperty<String> stringSimpleObjectProperty = this.rootModel.currentScriptProperty();
stringSimpleObjectProperty.bind(stringObservableValue);
// rootModel.currentScriptProperty().addListener((prop, old, cur) -> {clear(); insertText(0, cur););});
}
public void init() {
this.setWrapText(true);
this.setParagraphGraphicFactory(LineNumberFactory.get(this));
this.setDefaultText();
}
private void setDefaultText() {
this.appendText("script test(){\n\n}");
}
}
package edu.kit.formal.gui.model;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import javafx.beans.property.ListProperty;
import javafx.beans.property.SimpleListProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import java.io.File;
/**
* Model for the root window
* Created by sarah on 5/26/17.
*/
public class RootModel {
/**
* Current laoded ScriptFile
*/
private final SimpleObjectProperty<File> scriptFile;
/**
* Current loaded KeY File
*/
private final SimpleObjectProperty<File> keYFile;
/**
* Current loaded script string
*/
private final SimpleObjectProperty<String> currentScript;
/**
* The list of goal nodes in the current state (depending on interpreter state)
*/
private ListProperty<GoalNode<KeyData>> currentGoalNodes;
/**
* Current SelectedGoalNode
*/
private SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalNode;
public RootModel() {
scriptFile = new SimpleObjectProperty<>();
keYFile = new SimpleObjectProperty<>();
currentScript = new SimpleObjectProperty<>("");
currentSelectedGoalNode = new SimpleObjectProperty<>();
currentGoalNodes = new SimpleListProperty<>(FXCollections.observableArrayList());
}
public GoalNode<KeyData> getCurrentSelectedGoalNode() {
return currentSelectedGoalNode.get();
}
public void setCurrentSelectedGoalNode(GoalNode currentSelectedGoalNode) {
this.currentSelectedGoalNode.set(currentSelectedGoalNode);
}
public SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalNodeProperty() {
return currentSelectedGoalNode;
}
public File getScriptFile() {
return scriptFile.get();
}
public void setScriptFile(File scriptFile) {
this.scriptFile.set(scriptFile);
}
public SimpleObjectProperty<File> scriptFileProperty() {
return scriptFile;
}
public File getKeYFile() {
return keYFile.get();
}
public void setKeYFile(File keYFile) {
this.keYFile.set(keYFile);
}
public SimpleObjectProperty<File> keYFileProperty() {
return keYFile;
}
public String getCurrentScript() {
return currentScript.get();
}
public void setCurrentScript(String currentScript) {
this.currentScript.set(currentScript);
}
public SimpleObjectProperty<String> currentScriptProperty() {
return currentScript;
}
public ObservableList<GoalNode<KeyData>> getCurrentGoalNodes() {
return currentGoalNodes.get();
}
public void setCurrentGoalNodes(ObservableList<GoalNode<KeyData>> currentGoalNodes) {
this.currentGoalNodes.set(currentGoalNodes);
}
public ListProperty<GoalNode<KeyData>> currentGoalNodesProperty() {
return currentGoalNodes;
}
}
package edu.kit.formal.interpreter;
import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.ASTNode;
import lombok.Getter;
......
package edu.kit.formal.interpreter;
import com.google.common.collect.BiMap;
import com.google.common.collect.ImmutableBiMap;
import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.api.VariableAssignments;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.interpreter.data.Value;
import edu.kit.formal.interpreter.data.VariableAssignment;
import edu.kit.formal.interpreter.funchdl.CommandLookup;
......@@ -24,26 +27,29 @@ import java.util.logging.Logger;
public class Interpreter<T> extends DefaultASTVisitor<Void>
implements ScopeObservable {
private static final int MAX_ITERATIONS = 5;
@Getter
private static final BiMap<Type, VariableAssignments.VarType> typeConversionBiMap =
new ImmutableBiMap.Builder<Type, VariableAssignments.VarType>()
.put(Type.ANY, VariableAssignments.VarType.ANY)
.put(Type.BOOL, VariableAssignments.VarType.BOOL)
.put(Type.TERM, VariableAssignments.VarType.FORMULA) //TODO: parametrisierte Terms
.put(Type.INT, VariableAssignments.VarType.INT)
.put(Type.STRING, VariableAssignments.VarType.OBJECT)
.build();
private static Logger logger = Logger.getLogger("interpreter");
//TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
private Stack<State<T>> stateStack = new Stack<>();
@Getter
private List<Visitor> entryListeners = new ArrayList<>(),
exitListeners = new ArrayList<>();
@Getter
@Setter
private MatcherApi<T> matcherApi;
@Getter
private CommandLookup functionLookup;
@Getter
@Setter
private boolean scrictSelectedGoalMode = false;
@Getter
private ScriptApi scriptApi;
......@@ -152,7 +158,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
@Override
public Void visit(CasesStatement casesStatement) {
enterScope(casesStatement);
State<T> beforeCases = stateStack.pop();
State<T> beforeCases = stateStack.peek();
List<GoalNode<T>> allGoalsBeforeCases = beforeCases.getGoals();
......@@ -199,13 +205,13 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
}
stateStack.push(newStateAfterCases);
}
stateStack.peek().getGoals().removeAll(beforeCases.getGoals());
exitScope(casesStatement);
return null;
}
/**
* Match a set of goal nodes against a matchpattern of a case and return the metched goals together with instantiated variables
* Match a set of goal nodes against a matchpattern of a case and return the matched goals together with instantiated variables
*
* @param allGoalsBeforeCases
* @param aCase
......@@ -472,9 +478,6 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
return getCurrentState().getGoals();
}
public Type transKeYFormType(String keYDeclarationPrefix) {
//getType Map in interpreter for this create map in interpreter
return null;
}
//endregion
}
......@@ -7,7 +7,6 @@ import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.formal.ScopeLogger;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.funchdl.*;
import edu.kit.formal.proofscriptparser.Facade;
......
package edu.kit.formal.interpreter;
import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.api.ProjectedNode;
import de.uka.ilkd.key.api.ProofApi;
import de.uka.ilkd.key.api.ProofManagementApi;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.Facade;
import java.io.File;
import java.io.IOException;
/**
* Created by sarah on 5/29/17.
*/
public class KeYInterpreterFacade {
private ProofManagementApi pma;
private ProofApi pa;
private ProjectedNode currentRoot;
public State<KeyData> executeScriptWithKeYProblemFile(String currentScriptText, File keyProblemFile) {
Interpreter<KeyData> inter = buildKeYInterpreter(keyProblemFile);
ProjectedNode root = pa.getFirstOpenGoal();
KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof());
try {
inter.interpret(Facade.getAST(currentScriptText), new GoalNode<>(null, keyData));
return inter.getCurrentState();
} catch (IOException e) {
e.printStackTrace();
}
return null;
}
//TODO bei Aufruf ausfuehren
private Interpreter<KeyData> buildKeYInterpreter(File keYFile) {
InterpreterBuilder interpreterBuilder = new InterpreterBuilder();
Interpreter<KeyData> interpreter = null;
try {
pma = KeYApi.loadFromKeyFile(keYFile);
pa = pma.getLoadedProof();
interpreterBuilder.proof(pa).macros().scriptCommands();
pa.getProof().getProofIndependentSettings().getGeneralSettings().setOneStepSimplification(false);
interpreter = interpreterBuilder.build();
} catch (ProblemLoaderException e) {
e.printStackTrace();
}
return interpreter;
}
}