Commit a006bc8f authored by Alexander Weigl's avatar Alexander Weigl

Merge branch 'master' of git.scc.kit.edu:xt9634/ProofScriptParser

* 'master' of git.scc.kit.edu:xt9634/ProofScriptParser:
  Highlighting of node in proof tree, interactive mode now working a bit better
  Bugfix that removed/expanded nodes were still in state due to selectedGoalNode field
parents 400269f0 fe78f6e4
Pipeline #15280 failed with stages
in 1 minute and 34 seconds
......@@ -2,7 +2,6 @@ package edu.kit.iti.formal.psdbg.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.api.VariableAssignments;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
......@@ -66,7 +65,7 @@ public class KeyInterpreter extends Interpreter<KeyData> {
}
}
//prune proof
logger.debug("The closes script " + (allClosed ? "closed the proof.\n" : "did not close the proof.\n") + "Rolling Back proof now.");
LOGGER.debug("The closes script " + (allClosed ? "closed the proof.\n" : "did not close the proof.\n") + "Rolling Back proof now.");
Proof currentKeYproof = selectedGoalNode.getData().getProof();
ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode());
currentKeYproof.pruneProof(selectedGoalCopy.getData().getNode());
......
......@@ -15,6 +15,8 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import java.util.Collection;
......@@ -28,6 +30,8 @@ import java.util.Map;
*/
@RequiredArgsConstructor
public class MacroCommandHandler implements CommandHandler<KeyData> {
protected static Logger LOGGER = LogManager.getLogger(MacroCommandHandler.class);
@Getter
private final Map<String, ProofMacro> macros;
......@@ -57,6 +61,7 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
State<KeyData> state = interpreter.getCurrentState();
GoalNode<KeyData> expandedNode = state.getSelectedGoalNode();
assert state.getGoals().contains(expandedNode);
try {
......@@ -67,6 +72,8 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
ImmutableList<Goal> ngoals = expandedNode.getData().getProof().getSubtreeGoals(expandedNode.getData().getNode());
state.getGoals().remove(expandedNode);
state.setSelectedGoalNode(null);
if (ngoals.isEmpty()) {
Node start = expandedNode.getData().getNode();
//start.leavesIterator()
......@@ -74,7 +81,7 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
Iterator<Node> nodeIterator = start.leavesIterator();
while (nodeIterator.hasNext()) {
Node n = nodeIterator.next();
System.out.println(n.isClosed());
LOGGER.error(n.isClosed());
}
} else {
......@@ -83,6 +90,9 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
KeyData kdn = new KeyData(expandedNode.getData(), g.node());
state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode()));
}
assert !state.getGoals().contains(expandedNode);
}
}
} catch (InterruptedException e) {
......
......@@ -15,6 +15,8 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import java.util.Collection;
......@@ -30,6 +32,8 @@ import java.util.Map;
*/
@RequiredArgsConstructor
public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
protected static Logger LOGGER = LogManager.getLogger(ProofScriptCommandBuilder.class);
@Getter
private final Map<String, ProofScriptCommand> commands;
......@@ -65,7 +69,10 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
c.execute(uiControl, cc, estate);
//what happens if this is empty -> meaning proof is closed
state.getGoals().remove(expandedNode);
if (state.getSelectedGoalNode().equals(expandedNode)) {
state.setSelectedGoalNode(null);
}
ImmutableList<Goal> ngoals = kd.getProof().getSubtreeGoals(kd.getNode());
if (ngoals.isEmpty()) {
Node start = expandedNode.getData().getNode();
......@@ -74,7 +81,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
Iterator<Node> nodeIterator = start.leavesIterator();
while (nodeIterator.hasNext()) {
Node n = nodeIterator.next();
System.out.println(n.isClosed());
LOGGER.error(n.isClosed());
}
} else {
......@@ -83,7 +90,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode()));
}
}
state.getGoals().remove(expandedNode);
} catch (Exception e) {
throw new RuntimeException(e);
......
......@@ -68,6 +68,9 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
ImmutableList<Goal> ngoals = kd.getProof().getSubtreeGoals(kd.getNode());
state.getGoals().remove(expandedNode);
if (state.getSelectedGoalNode().equals(expandedNode)) {
state.setSelectedGoalNode(null);
}
for (Goal g : ngoals) {
KeyData kdn = new KeyData(kd, g.node());
state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
......
......@@ -221,6 +221,9 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
}
State<T> stateAfterCase = popState(); //remove state from stack
if (stateAfterCase.getSelectedGoalNode() != null) {
assert stateAfterCase.getGoals().contains(stateAfterCase.getSelectedGoalNode());
}
if (result && stateAfterCase.getGoals() != null) {
resultingGoals.addAll(stateAfterCase.getGoals());
......@@ -273,6 +276,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
Expression matchExpression = guardedCaseStatement.getGuard();
State<T> currentStateToMatch = peekState();
GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
assert currentStateToMatch.getGoals().contains(selectedGoal);
VariableAssignment va = evaluateMatchInGoal(matchExpression, selectedGoal);
try {
......@@ -510,6 +514,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
enterScope(caseStmts);
goalNode.enterScope(va);
State<T> s = newState(goalNode);
assert s.getGoals().contains(s.getSelectedGoalNode());
caseStmts.accept(this);
//popState(s); //This may be incorrect-> Bug? -> Cases Statement needs to pop, as goals need to be collected
exitScope(caseStmts);
......@@ -644,7 +649,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
//region State Handling
public GoalNode<T> getSelectedNode() {
try {
return stateStack.peek().getSelectedGoalNode();
GoalNode<T> selectedGoalNode = stateStack.peek().getSelectedGoalNode();
if (selectedGoalNode != null) {
assert stateStack.peek().getGoals().contains(selectedGoalNode);
}
return selectedGoalNode;
} catch (IllegalStateException e) {
if (scrictSelectedGoalMode)
throw e;
......
......@@ -79,10 +79,6 @@ public class State<T> {
return new State<T>(copiedGoals, refToSelGoal);
}
public void setSelectedGoalNode(GoalNode<T> gn) {
this.selectedGoalNode = gn;
}
public GoalNode<T> getSelectedGoalNode() {
/* if (selectedGoalNode == null) {
throw new IllegalStateException("no selected node");
......@@ -96,9 +92,17 @@ public class State<T> {
if (getGoals().size() == 1) {
selectedGoalNode = getGoals().get(0);
}
return selectedGoalNode;
}
public void setSelectedGoalNode(GoalNode<T> gn) {
if (gn != null) {
assert goals.contains(gn);
}
this.selectedGoalNode = gn;
}
public String toString() {
if (selectedGoalNode == null) {
return "No Goal selected";
......
......@@ -103,7 +103,7 @@ public class ProofScriptDebugger extends Application {
logger.info("KeY: " + KeYConstants.COPYRIGHT);
logger.info("KeY Version: " + KeYConstants.VERSION);
logger.info("KeY Internal: " + KeYConstants.INTERNAL_VERSION);
//logger.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
//LOGGER.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
} catch (Exception e) {
......
......@@ -26,6 +26,7 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import javafx.application.Platform;
......@@ -80,10 +81,14 @@ public class DebuggerMain implements Initializable {
protected static final Logger LOGGER = LogManager.getLogger(DebuggerMain.class);
public final ContractLoaderService contractLoaderService = new ContractLoaderService();
private InspectionViewsController inspectionViewsController;
private final ExecutorService executorService = Executors.newFixedThreadPool(2);
@Getter
private final DebuggerMainModel model = new DebuggerMainModel();
private InspectionViewsController inspectionViewsController;
private ScriptController scriptController;
@FXML
......@@ -123,7 +128,7 @@ public class DebuggerMain implements Initializable {
private CheckMenuItem miProofTree;
@FXML
private ToggleButton btnIM;
private ToggleButton btnInteractiveMode;
private JavaArea javaArea = new JavaArea();
......@@ -194,6 +199,7 @@ public class DebuggerMain implements Initializable {
model.setDebugMode(false);
scriptController = new ScriptController(dockStation);
interactiveModeController = new InteractiveModeController(scriptController);
btnInteractiveMode.setSelected(false);
inspectionViewsController = new InspectionViewsController(dockStation);
activeInspectorDock = inspectionViewsController.getActiveInterpreterTabDock();
//register the welcome dock in the center
......@@ -857,15 +863,16 @@ public class DebuggerMain implements Initializable {
@FXML
public void interactiveMode(ActionEvent actionEvent) {
if (btnIM.isSelected()) {
interactiveModeController.stop();
} else {
if (btnInteractiveMode.isSelected()) {
interactiveModeController.setActivated(true);
interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel());
} else {
interactiveModeController.stop();
}
}
}
@FXML
public void showWelcomeDock(ActionEvent actionEvent) {
if (!welcomePaneDock.isDocked() && !welcomePaneDock.isFloating()) {
......
......@@ -67,7 +67,7 @@ public class InteractiveModeController {
public void stop() {
Events.unregister(this);
String c = getCasesAsString();
scriptController.getDockNode(scriptArea).undock();
scriptController.getDockNode(scripundocktArea).undock();
Events.fire(new Events.InsertAtTheEndOfMainScript(c));
}
......
......@@ -309,17 +309,19 @@ public class ProofTree extends BorderPane {
}
if (n.childrenCount() == 0) {
ti.getChildren().add(new TreeItem<>(new TreeNode(
n.isClosed() ? "CLOSED GOAL" : "OPEN GOAL", null)));
TreeItem<TreeNode> e = new TreeItem<>(new TreeNode(
n.isClosed() ? "CLOSED GOAL" : "OPEN GOAL", null));
ti.getChildren().add(e);
return ti;
}
Node node = n.child(0);
if (n.childrenCount() == 1) {
ti.getChildren().add(new TreeItem<>(new TreeNode(toString(node), node)));
ti.getChildren().add(new TreeItem<>(new TreeNode(node.serialNr() + ": " + toString(node), node)));
while (node.childrenCount() == 1) {
node = node.child(0);
ti.getChildren().add(new TreeItem<>(new TreeNode(toString(node), node)));
ti.getChildren().add(new TreeItem<>(new TreeNode(node.serialNr() + ": " + toString(node), node)));
}
}
......@@ -364,20 +366,24 @@ public class ProofTree extends BorderPane {
}
};
tftc.setConverter(stringConverter);
//tftc.itemProperty().addListener((p, o, n) -> repaint(tftc));
tftc.itemProperty().addListener((p, o, n) -> {
if (n != null)
repaint(tftc);
});
//colorOfNodes.addListener((InvalidationListener) o -> repaint(tftc));
return tftc;
}
/*private void repaint(TextFieldTreeCell<TreeNode> tftc) {
private void repaint(TextFieldTreeCell<TreeNode> tftc) {
Node n = tftc.getItem().node;
tftc.setStyle("");
if (n != null) {
if (n != null && n.leaf()) {
if (n.isClosed()) {
colorOfNodes.putIfAbsent(n, "green");
colorOfNodes.putIfAbsent(n, "seagreen");
//tftc.setStyle("-fx-background-color: greenyellow");
} else {
colorOfNodes.putIfAbsent(n, "darkred");
}
if (colorOfNodes.containsKey(n)) {
tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";");
......@@ -385,7 +391,7 @@ public class ProofTree extends BorderPane {
}
expandRootToItem(tftc.getTreeItem());
}*/
}
public Object getColorOfNodes() {
return colorOfNodes.get();
......
......@@ -15,8 +15,6 @@ import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue;
import javafx.collections.FXCollections;
import javafx.collections.ObservableMap;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.apache.commons.io.FileUtils;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
......@@ -122,6 +120,7 @@ public class ScriptController {
return getDockNode(findEditor(filepath));
}
<<<<<<< HEAD
public DockNode getDockNode(ScriptArea editor) {
if (editor == null) {
return null;
......@@ -162,6 +161,8 @@ public class ScriptController {
}
}
=======
>>>>>>> fe78f6e478dd00993310329ee09e52cb3af7a516
/**
* Create new DockNode for ScriptArea Tab
*
......@@ -200,6 +201,46 @@ public class ScriptController {
return dockNode;
}
/**
* Create a new Tab in the ScriptTabPane containing the contents of the file given as argument
*
* @param filePath to file that should be loaded to new tab
* @return refernce to new scriptArea in new tab
* @throws IOException if an Exception occurs while loading file
*/
public ScriptArea createNewTab(File filePath) throws IOException {
filePath = filePath.getAbsoluteFile();
if (findEditor(filePath) == null) {
ScriptArea area = new ScriptArea();
area.mainScriptProperty().bindBidirectional(mainScript);
area.setFilePath(filePath);
DockNode dockNode = createDockNode(area);
openScripts.put(area, dockNode);
if (filePath.exists()) {
String code = FileUtils.readFileToString(filePath, "utf-8");
if (!area.textProperty().getValue().isEmpty()) {
area.deleteText(0, area.textProperty().getValue().length());
}
area.setText(code);
}
return area;
} else {
logger.info("File already exists. Will not load it again");
ScriptArea area = findEditor(filePath);
return area;
}
}
public DockNode getDockNode(ScriptArea editor) {
if (editor == null) {
return null;
}
return openScripts.get(editor);
}
/**
* Get all breakpoints in the current area
*
......
......@@ -6,17 +6,26 @@ script test(){
exLeft;
andLeft;
eqSymm formula = `agatha = butler`;
nnf_imp2or formula=`\foral S w6;(hates(agatha,w6) -> hates(butler,w6))`;
nnf_imp2or formula=`\forall S w6;(hates(agatha,w6) -> hates(butler,w6))`;
}
script SolveAgathaRiddle_1() {
impRight;
andLeft;
notLeft;
repeat { andLeft; }
exLeft;
andLeft;
eqSymm formula = `agatha = butler`;
auto;
}
script SolveAgathaRiddle_2() {
impRight;
andLeft;
notLeft;
andLeft;
andLeft;
andLeft;
......@@ -27,27 +36,12 @@ script SolveAgathaRiddle_1() {
andLeft;
andLeft;
andLeft;
exLeft;
andLeft;
eqSymm formula = `agatha = butler`;
auto;
//nnf_imp2or on= `hates(agatha, w6) -> hates(butler, w6)`;
//nnf_imp2or; -> wirft hier ScriptCommandNotApplicableException
//wirft ansonsten immer java.lang.RuntimeException: de.uka.ilkd.key.macros.scripts.meta.ConversionException: Could not convert value hates(agatha, w6) -> hates(butler, w6) to type interface de.uka.ilkd.key.logic.Term
// at
//nnf_imp2or formula= `hates(agatha, w6) -> hates(butler, w6)`;
//nnf_imp2or on = `hates(agatha, w6) -> hates(butler, w6)` formula=` \forall S w6; (hates(agatha, w6) -> hates(butler, w6))`;
}
script SolveAgathaRiddle_2() {
impRight;
andLeft;
notLeft;
repeat { andLeft; }
exLeft;
andLeft;
eqSymm formula = `agatha = butler`;
nnf_imp2or formula=`\forall S w6;(hates(agatha,w6) -> hates(butler,w6))`;
auto;
}
......@@ -10,7 +10,6 @@ class Bubblesort {
public int[] bubbleSort(int[] arr) {
int temp = 0;
/*@
@ loop_invariant 0 <= i && i <= arr.length;
@ loop_invariant (\forall int a,b; a >= arr.length - i && b <= arr.length && a < b && i > 0; arr[a] <= arr[b]);
......@@ -18,7 +17,6 @@ class Bubblesort {
@ decreases arr.length - i;
@*/
for(int i=0; i < arr.length; i++){
/*@
@ loop_invariant 1 <= j && j <= arr.length - i + 1;
@ assignable arr[*], temp;
......@@ -41,7 +39,7 @@ class Bubblesort {
/*@ public normal_behaviour
@ requires arr != null;
@ requires arr.length > 0;
@ ensures true;
@ ensures \result == true;
@*/
public boolean test(int[] arr) {
arr = bubbleSort(arr);
......
......@@ -3,36 +3,8 @@ script t1(){
cases{
case match `?X >= 0,?X > 0 ==>`:
cut `?X = 0`[?X \ X];
foreach{
auto;
}
//foreach{
// auto;
//}
}
script t2(){
symbex;
cases{
case match '.*x.*':
auto;
default:
auto;
}
}
script t(){
symbex;
foreach{
simp_heap;
}
}
......@@ -9,7 +9,6 @@
<?import javafx.scene.layout.Pane?>
<?import javafx.scene.layout.VBox?>
<?import org.dockfx.DockPane?>
<?import org.controlsfx.control.ToggleSwitch?>
<BorderPane xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane" xmlns="http://javafx.com/javafx/8.0.112"
fx:controller="edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain"
prefWidth="1024" prefHeight="640">
......@@ -276,7 +275,7 @@
</tooltip>
</Button>
<ToggleButton fx:id="btnIM" onAction="#interactiveMode" disable="true">
<ToggleButton fx:id="btnInteractiveMode" onAction="#interactiveMode" disable="true">
<!--disable="${! controller.debugMode}"-->
<graphic>
<MaterialDesignIconView glyphName="HAND_POINTING_RIGHT" size="24.0"/>
......
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