Commit 8f51e69a authored by Sarah Grebing's avatar Sarah Grebing

First version of separate thread for building proofenvironment

parent 02365c55
Pipeline #10821 failed with stage
in 1 minute and 20 seconds
......@@ -3,10 +3,9 @@ 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.KeYProofFacade;
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;
......@@ -20,6 +19,8 @@ import java.io.File;
import java.net.URL;
import java.util.List;
import java.util.ResourceBundle;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
/**
* Controller for the Debugger MainWindow
......@@ -62,6 +63,8 @@ public class DebuggerMainWindowController implements Initializable {
* **********************************************************************************************************/
@FXML
ListGoalView goalView;
ExecutorService executorService = null;
KeYProofFacade facade;
private RootModel model;
@Setter
private Interpreter<KeyData> interpreter;
......@@ -72,16 +75,9 @@ public class DebuggerMainWindowController implements Initializable {
@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();
facade.executeScript(model.getCurrentScript());
List<GoalNode<KeyData>> g = model.getCurrentState().getGoals();
this.model.getCurrentGoalNodes().addAll(g);
buttonStartInterpreter.setText("execute Script");
}
......@@ -108,6 +104,7 @@ public class DebuggerMainWindowController implements Initializable {
protected void loadKeYFile() {
File keyFile = openFileChooserDialog("Select KeY File", "KeY Files", "key", "java", "script");
this.model.setKeYFile(keyFile);
buildKeYProofFacade();
}
......@@ -137,6 +134,7 @@ public class DebuggerMainWindowController implements Initializable {
}
public void init() {
facade = new KeYProofFacade(this.model);
scriptArea.setRootModel(this.model);
scriptArea.init();
goalView.setRootModel(this.model);
......@@ -149,4 +147,16 @@ public class DebuggerMainWindowController implements Initializable {
public void initialize(URL location, ResourceBundle resources) {
}
private void buildKeYProofFacade() {
executorService = Executors.newFixedThreadPool(2);
executorService.execute(() -> {
facade = new KeYProofFacade(model);
facade.buildKeYInterpreter(model.getKeYFile());
});
executorService.shutdown();
}
}
......@@ -3,11 +3,13 @@ package edu.kit.formal.gui.model;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State;
import javafx.beans.property.ListProperty;
import javafx.beans.property.SimpleListProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import lombok.Getter;
import java.io.File;
......@@ -42,6 +44,9 @@ public class RootModel {
*/
private SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalNode;
@Getter
private State<KeyData> currentState;
public RootModel() {
scriptFile = new SimpleObjectProperty<>();
......@@ -113,4 +118,7 @@ public class RootModel {
}
public void setCurrentState(State<KeyData> currentState) {
this.currentState = currentState;
}
}
......@@ -5,10 +5,13 @@ 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.gui.model.RootModel;
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.exceptions.InterpreterRuntimeException;
import edu.kit.formal.proofscriptparser.Facade;
import lombok.Getter;
import java.io.File;
import java.io.IOException;
......@@ -16,21 +19,33 @@ import java.io.IOException;
/**
* Created by sarah on 5/29/17.
*/
public class KeYInterpreterFacade {
public class KeYProofFacade {
@Getter
private ProofManagementApi pma;
@Getter
private ProofApi pa;
@Getter
private ProjectedNode currentRoot;
private RootModel model;
@Getter
private Interpreter<KeyData> interpreter;
public KeYProofFacade(RootModel model) {
this.model = model;
}
public State<KeyData> executeScriptWithKeYProblemFile(String currentScriptText, File keyProblemFile) {
Interpreter<KeyData> inter = buildKeYInterpreter(keyProblemFile);
ProjectedNode root = pa.getFirstOpenGoal();
buildKeYInterpreter(keyProblemFile);
currentRoot = pa.getFirstOpenGoal();
KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof());
KeyData keyData = new KeyData(currentRoot.getProofNode(), pa.getEnv(), pa.getProof());
try {
inter.interpret(Facade.getAST(currentScriptText), new GoalNode<>(null, keyData));
return inter.getCurrentState();
interpreter.interpret(Facade.getAST(currentScriptText), new GoalNode<>(null, keyData));
return interpreter.getCurrentState();
} catch (IOException e) {
e.printStackTrace();
}
......@@ -38,21 +53,49 @@ public class KeYInterpreterFacade {
}
//TODO bei Aufruf ausfuehren
private Interpreter<KeyData> buildKeYInterpreter(File keYFile) {
/**
* Build the KeYInterpreter that handles the execution of the loaded key problem file
*
* @param keYFile
*/
public void buildKeYInterpreter(File keYFile) {
InterpreterBuilder interpreterBuilder = new InterpreterBuilder();
Interpreter<KeyData> interpreter = null;
this.interpreter = null;
try {
pma = KeYApi.loadFromKeyFile(keYFile);
pa = pma.getLoadedProof();
interpreterBuilder.proof(pa).macros().scriptCommands();
pa.getProof().getProofIndependentSettings().getGeneralSettings().setOneStepSimplification(false);
interpreter = interpreterBuilder.build();
this.interpreter = interpreterBuilder.build();
} catch (ProblemLoaderException e) {
e.printStackTrace();
}
return interpreter;
}
/**
* Execute ScriptFile in the created interpreter
*
* @param
*/
public void executeScript(String scriptText) throws InterpreterRuntimeException {
if (interpreter == null) {
throw new InterpreterRuntimeException("No interpreter created");
}
ProjectedNode root = pa.getFirstOpenGoal();
KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof());
try {
interpreter.interpret(Facade.getAST(scriptText), new GoalNode<KeyData>(null, keyData));
this.model.setCurrentState(interpreter.getCurrentState());
} catch (IOException e) {
e.printStackTrace();
}
}
}
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