Skip to content

GitLab

Commit 591415cf authored by Alexander Weigl's avatar Alexander Weigl
Browse files

working on new ProofTree view

parent 35f07285
Pipeline #22015 passed with stages
in 5 minutes and 32 seconds
Expand all Hide whitespace changes
Inline Side-by-side
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/SavepointVisitor.java
View file @ 591415cf
package edu.kit.iti.formal.psdbg.parser;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.util.Pair;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.Parameters;
......
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java
View file @ 591415cf
......@@ -166,4 +166,12 @@ public abstract class ASTNode<T extends ParserRuleContext>
public int hashCode() {
return Objects.hash(getRuleContext());
}
public int getSyntaxWidth() {
if (ruleContext != null) {
return ruleContext.stop.getStopIndex()
- ruleContext.start.getStartIndex();
}
return -1;
}
}
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java
View file @ 591415cf
......@@ -16,7 +16,6 @@ import javafx.beans.binding.BooleanBinding;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.concurrent.Task;
import jdk.nashorn.internal.objects.annotations.Getter;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
......
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java
View file @ 591415cf
......@@ -23,6 +23,8 @@ 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.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDeclaredException;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDefinedException;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.Variable;
import lombok.Getter;
......@@ -154,7 +156,11 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
private Map<String, Object> createParameters(VariableAssignment assignments) {
Map<String, Object> params = new HashMap<>();
for (String s : MAGIC_PARAMETER_NAMES) {
params.put(s, assignments.getValue(new Variable(Variable.MAGIC_PREFIX + s)));
try {
params.put(s, assignments.getValue(new Variable(Variable.MAGIC_PREFIX + s)));
} catch (VariableNotDefinedException | VariableNotDeclaredException e) {
}
}
return params;
}
......
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/PTreeNode.java
View file @ 591415cf
......@@ -4,6 +4,7 @@ import edu.kit.iti.formal.psdbg.ShortCommandPrinter;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.CaseStatement;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
......@@ -11,6 +12,7 @@ import lombok.Setter;
import javax.annotation.Nullable;
import java.util.*;
import java.util.stream.Collectors;
/**
* PTreeNode represents a node in the state graph.
......@@ -111,11 +113,21 @@ public class PTreeNode<T> {
/**
* Calculate a span of bytes of the syntactical representation.
*
* @return
*/
int getSyntaxWidth() {
return getStatement().getRuleContext().stop.getStopIndex()
- getStatement().getRuleContext().start.getStartIndex();
return getStatement().getSyntaxWidth();
}
public Collection<GoalNode<T>> getMutatedNodes() {
if (statement instanceof CallStatement) {//TODO better predicate for mutators
return Collections.emptyList();
}
assert stateAfterStmt != null && stateBeforeStmt != null;
ArrayList<PTreeNode<T>> list = new ArrayList<>();
GoalNode<T> incoming = stateBeforeStmt.getSelectedGoalNode();
return stateAfterStmt.getGoals().stream().filter(gn -> gn.getParent() == incoming).collect(Collectors.toList());
}
}
\ No newline at end of file
ui/build.gradle
View file @ 591415cf
......@@ -19,11 +19,14 @@ lessCompile {
processResources.dependsOn lessCompile
dependencies {
compile group: 'de.jensd', name: 'fontawesomefx-materialdesignfont', version: '2.0.26-9.1.2'
compile group: 'de.jensd', name: 'fontawesomefx-commons', version: '9.1.2'
compile group: 'de.jensd', name: 'fontawesomefx-materialdesignfont', version: '1.7.22-4'
compile group: 'de.jensd', name: 'fontawesomefx-commons', version: '8.15'
// compile group: 'de.jensd', name: 'fontawesomefx-materialdesignfont', version: '2.0.26-9.1.2'
// compile group: 'de.jensd', name: 'fontawesomefx-commons', version: '9.1.2'
compile group: 'org.fxmisc.richtext', name: 'richtextfx', version: '0.9.0'
//compile group: 'org.fxmisc.richtext', name: 'richtextfx', version: '1.0.0-SNAPSHOT'
compile group: 'org.controlsfx', name: 'controlsfx', version: '9.0.0'
compile group: 'org.controlsfx', name: 'controlsfx', version: '8.40.12'
compile group: 'org.antlr', name: 'antlr4', version: '4.7'
antlr group: 'org.antlr', name: 'antlr4', version: '4.7'
......@@ -36,7 +39,7 @@ dependencies {
def mainClassName = 'edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger'
task runApp(type: JavaExec) {
jvmArgs << '-Dsun.awt.disablegrab=true' << '-Dglass.disableGrab=true'
/*applicationDefaultJvmArgs = [
// For accessing VirtualFlow field from the base class in GridViewSkin
"--add-opens=javafx.controls/javafx.scene.control.skin=ALL-UNNAMED",
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java
View file @ 591415cf
......@@ -8,8 +8,6 @@ import javafx.application.Platform;
import javafx.fxml.FXMLLoader;
import javafx.scene.Parent;
import javafx.scene.Scene;
import javafx.scene.input.KeyCode;
import javafx.scene.input.KeyCodeCombination;
import javafx.stage.Stage;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
......@@ -32,10 +30,8 @@ public class ProofScriptDebugger extends Application {
public static final String VERSION = "Experimental-1.1";
public static final String KEY_VERSION = KeYConstants.VERSION;
private Logger logger = LogManager.getLogger("psdbg");
private static Logger consoleLogger = LogManager.getLogger("console");
private Logger logger = LogManager.getLogger("psdbg");
public static void main(String[] args) {
launch(args);
......@@ -50,11 +46,15 @@ public class ProofScriptDebugger extends Application {
DebuggerMain controller = fxmlLoader.getController();
Scene scene = new Scene(root);
primaryStage.setOnCloseRequest(event -> Platform.exit());
scene.getStylesheets().addAll(
getClass().getResource("debugger-ui.css").toExternalForm(),
DockNode.class.getResource("default.css").toExternalForm()
);
logger.info("Loading CSS class " + getClass().getResource("debugger-ui.css").toExternalForm());
try {
scene.getStylesheets().addAll(
getClass().getResource("debugger-ui.css").toExternalForm(),
DockNode.class.getResource("default.css").toExternalForm()
);
logger.info("Loading CSS class " + getClass().getResource("debugger-ui.css").toExternalForm());
} catch (NullPointerException e) {
consoleLogger.error(e);
}
primaryStage.setTitle(NAME + " (" + VERSION + ") with KeY:" + KEY_VERSION);
primaryStage.setScene(scene);
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @ 591415cf
......@@ -155,7 +155,7 @@ public class DebuggerMain implements Initializable {
new MaterialDesignIconView(MaterialDesignIcon.CODEPEN)
);
//-----------------------------------------------------------------------------------------------------------------
private ProofTree proofTree = new ProofTree();
private ProofTree proofTree = new ProofTree(this);
private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree");
private WelcomePane welcomePane = new WelcomePane(this);
private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT));
......@@ -1334,7 +1334,7 @@ public class DebuggerMain implements Initializable {
GoalNode<KeyData> beforeNode = original.getStateBeforeStmt().getSelectedGoalNode();
List<GoalNode<KeyData>> stateAfterStmt = original.getStateAfterStmt().getGoals();
ProofTree ptree = new ProofTree();
ProofTree ptree = new ProofTree(DebuggerMain.this);
Proof proof = beforeNode.getData().getProof();
Node pnode = beforeNode.getData().getNode();
......@@ -1342,7 +1342,7 @@ public class DebuggerMain implements Initializable {
ptree.setProof(proof);
ptree.setRoot(pnode);
ptree.addNodeColor(pnode, "blueviolet");
ptree.setNodeColor(pnode, "blueviolet");
ptree.setDeactivateRefresh(true);
if (stateAfterStmt.size() > 0) {
......@@ -1351,7 +1351,7 @@ public class DebuggerMain implements Initializable {
.map(Goal::node)
.collect(Collectors.toSet());
ptree.getSentinels().addAll(sentinels);
sentinels.forEach(node -> ptree.addNodeColor(node, "blueviolet"));
sentinels.forEach(node -> ptree.setNodeColor(node, "blueviolet"));
} else {
Set<Node> sentinels = new HashSet<>();
Iterator<Node> nodeIterator = beforeNode.getData().getNode().leavesIterator();
......@@ -1361,7 +1361,7 @@ public class DebuggerMain implements Initializable {
sentinels.add(next);
}
ptree.getSentinels().addAll(sentinels);
sentinels.forEach(node -> ptree.addNodeColor(node, "blueviolet"));
sentinels.forEach(node -> ptree.setNodeColor(node, "blueviolet"));
//traverseProofTreeAndAddSentinelsToLeaves();
}
......@@ -1391,7 +1391,7 @@ public class DebuggerMain implements Initializable {
GoalNode<KeyData> beforeNode = stepInvOver.getStateBeforeStmt().getSelectedGoalNode();
List<GoalNode<KeyData>> stateAfterStmt = stepInvOver.getStateAfterStmt().getGoals();
ProofTree ptree = new ProofTree();
ProofTree ptree = new ProofTree(DebuggerMain.this);
Proof proof = beforeNode.getData().getProof();
Node pnode = beforeNode.getData().getNode();
......@@ -1399,7 +1399,7 @@ public class DebuggerMain implements Initializable {
ptree.setProof(proof);
ptree.setRoot(pnode);
ptree.addNodeColor(pnode, "blueviolet");
ptree.setNodeColor(pnode, "blueviolet");
ptree.setDeactivateRefresh(true);
if (stateAfterStmt.size() > 0) {
......@@ -1408,7 +1408,7 @@ public class DebuggerMain implements Initializable {
.map(Goal::node)
.collect(Collectors.toSet());
ptree.getSentinels().addAll(sentinels);
sentinels.forEach(node -> ptree.addNodeColor(node, "blueviolet"));
sentinels.forEach(node -> ptree.setNodeColor(node, "blueviolet"));
} else {
Set<Node> sentinels = new HashSet<>();
Iterator<Node> nodeIterator = beforeNode.getData().getNode().leavesIterator();
......@@ -1418,7 +1418,7 @@ public class DebuggerMain implements Initializable {
sentinels.add(next);
}
ptree.getSentinels().addAll(sentinels);
sentinels.forEach(node -> ptree.addNodeColor(node, "blueviolet"));
sentinels.forEach(node -> ptree.setNodeColor(node, "blueviolet"));
//traverseProofTreeAndAddSentinelsToLeaves();
}
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTreeContextMenu.java 0 → 100644
View file @ 591415cf
package edu.kit.iti.formal.psdbg.gui.controls;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
import de.uka.ilkd.key.pp.LogicPrinter;
import edu.kit.iti.formal.psdbg.LabelFactory;
import edu.kit.iti.formal.psdbg.gui.controller.Events;
import javafx.scene.control.Menu;
import javafx.scene.control.MenuItem;
import javafx.scene.control.SeparatorMenuItem;
import java.util.Arrays;
import java.util.List;
/**
* @author Alexander Weigl
* @version 1 (24.05.18)
*/
public class ProofTreeContextMenu extends javafx.scene.control.ContextMenu {
MenuItem copyBranchLabel = new MenuItem("Branch Label");
MenuItem copyProgramLines = new MenuItem("Program Lines");
MenuItem createCases = new MenuItem("Created Case for Open Goals");
MenuItem refresh = new MenuItem("Refresh");
MenuItem showSequent = new MenuItem("Show Sequent");
MenuItem showGoal = new MenuItem("Show in Goal List");
MenuItem expandAllNodes = new MenuItem("Expand Tree");
private ProofTree proofTree;
public ProofTreeContextMenu(ProofTree proofTree) {
this.proofTree = proofTree;
refresh.setOnAction(event -> proofTree.repopulate());
refresh.setGraphic(new MaterialDesignIconView(MaterialDesignIcon.REFRESH));
copyBranchLabel.setOnAction(evt -> proofTree.consumeNode(n -> Utils.intoClipboard(
LabelFactory.getBranchingLabel(n)), "Copied!"));
copyProgramLines.setOnAction(evt -> {
proofTree.consumeNode(n -> {
Utils.intoClipboard(
LabelFactory.getProgramLines(n));
}, "Copied!");
});
MenuItem copySequent = new MenuItem("Sequent");
copySequent.setOnAction(evt -> {
proofTree.consumeNode(n -> {
assert proofTree.getServices() != null : "set KeY services!";
String s = LogicPrinter.quickPrintSequent(n.sequent(), proofTree.getServices());
Utils.intoClipboard(s);
}, "Copied!");
});
MenuItem copyRulesLabel = new MenuItem("Rule labels");
copyRulesLabel.setOnAction(evt -> {
proofTree.consumeNode(n -> {
Utils.intoClipboard(
LabelFactory.getRuleLabel(n));
}, "Copied!");
});
MenuItem copyProgramStatements = new MenuItem("Statements");
copyProgramStatements.setOnAction(event -> {
proofTree.consumeNode(n -> {
Utils.intoClipboard(
LabelFactory.getProgramStatmentLabel(n));
}, "Copied!");
});
Menu copy = new Menu("Copy", new MaterialDesignIconView(MaterialDesignIcon.CONTENT_COPY),
copyBranchLabel, copyProgramLines,
copyProgramStatements, copyRulesLabel,
copySequent);
createCases.setOnAction(this::onCreateCases);
showSequent.setOnAction((evt) ->
proofTree.consumeNode(n -> Events.fire(new Events.ShowSequent(n)), ""));
showGoal.setOnAction((evt) -> proofTree.consumeNode(n -> Events.fire(new Events.SelectNodeInGoalList(n)), "Found!"));
expandAllNodes.setOnAction((event) -> {
proofTree.expandRootToLeaves(proofTree.getTreeProof().getRoot());
});
getItems().setAll(refresh, expandAllNodes, new SeparatorMenuItem(), copy, createCases, showSequent, showGoal);
setAutoFix(true);
setAutoHide(true);
}
public void onCreateCases(javafx.event.ActionEvent evt) {
if (proofTree.getProof() == null) {
return;
}
List<String[]> labels = LabelFactory.getLabelOfOpenGoals(proofTree.getProof(),
LabelFactory::getBranchingLabel);
String text;
if (labels.isEmpty()) {
text = "// no open goals";
} else if (labels.size() == 1) {
text = "// only one goal";
} else {
int upperLimit = 0;
/* trying to find the common suffix*/
try {
String[] ref = labels.get(0);
for (; true; upperLimit++) {
for (String[] lbl : labels) {
if (!lbl[upperLimit].equals(ref[upperLimit])) {
break;
}
}
upperLimit++;
}
} catch (ArrayIndexOutOfBoundsException e) {
}
int finalUpperLimit = upperLimit;
text = labels.stream()
.map(a -> Arrays.stream(a, finalUpperLimit, a.length))
.map(s -> s.reduce((a, b) -> b + LabelFactory.SEPARATOR + a).orElse("error"))
.map(s -> String.format("\tcase match \"%s\" :\n\t\t//commands", s))
.reduce((a, b) -> a + "\n" + b)
.orElse("ERROR");
}
String s = "cases {\n" + text + "\n}";
Events.fire(new Events.InsertAtTheEndOfMainScript(s));
Events.fire(new Events.PublishMessage("Copied to Clipboard"));
}
}
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