From 3129e863ab8af8dd51f805399d9408fd8ea52c8b Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Mon, 9 Apr 2018 13:32:27 +0200 Subject: [PATCH] Bugfix in deepcopy of goal nodes: showed itself wehn using variables declared before a try statement --- .../psdbg/interpreter/KeyInterpreter.java | 1 - .../formal/psdbg/interpreter/Interpreter.java | 6 +++--- .../formal/psdbg/interpreter/data/GoalNode.java | 17 ++++++++++++++--- .../formal/psdbg/gui/controls/ScriptArea.java | 2 +- .../formal/psdbg/gui/controls/SequentView.java | 2 +- .../iti/formal/psdbg/gui/controls/Utils.java | 6 +++--- .../psdbg/examples/contraposition/script.kps | 9 +++++++++ 7 files changed, 31 insertions(+), 12 deletions(-) diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java index f1805d9f..2547f8fa 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java @@ -99,7 +99,6 @@ public class KeyInterpreter extends Interpreter { logger.debug(String.format("Beginning of suspicion execution of %s", statements)); GoalNode goalNode = getSelectedNode(); pushState(new State<>(goalNode.deepCopy())); // copy for later prove - List backupExitListener = getExitListeners(), backupEntryListener = getEntryListeners(); try { diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java index 2c27a554..862d3861 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java @@ -454,13 +454,13 @@ public class Interpreter extends DefaultASTVisitor exitScope(casesStatement); return null; }*/ - @Override + /* @Override public Object visit(TryCase TryCase) { enterScope(TryCase); - + //is handled by KeYInterpreter exitScope(TryCase); return false; - } + }*/ /** * Evaluate a match in a specific goal diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java index 54e76707..d7b734ac 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java @@ -29,7 +29,7 @@ public class GoalNode { private boolean isClosed; /** - * This conctructur will be replaced with concrete one that uses projectedNode + * * * @param parent * @param data @@ -41,6 +41,12 @@ public class GoalNode { this.data = data; this.isClosed = isClosed; } + private GoalNode(GoalNode parent, VariableAssignment assignments, T data, boolean isClosed) { + this.assignments = assignments.deepCopy(); + this.parent = parent; + this.data = data; + this.isClosed = isClosed; + } /** * @param varname @@ -104,8 +110,13 @@ public class GoalNode { } public GoalNode deepCopy() { - //TODO method does nothing helpful atm - return new GoalNode(parent, data, isClosed); + if (parent != null) { + return new GoalNode(parent.deepCopy(), data, isClosed); + } else { + return new GoalNode(parent, assignments.deepCopy(), data, isClosed); + } + + } public VariableAssignment enterScope(VariableAssignment va) { diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java index 62ea6b2f..9b721a89 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java @@ -280,7 +280,7 @@ public class ScriptArea extends BorderPane { LOGGER.debug("ScriptArea.updateMainScriptMarker"); if (ms != null && filePath.get().getAbsolutePath().equals(ms.getSourceName())) { - System.out.println(ms); + LOGGER.debug("ScriptArea.updateIdentifier"+ ms); CharStream stream = CharStreams.fromString(codeArea.getText(), filePath.get().getAbsolutePath()); Optional ps = ms.find(Facade.getAST(stream)); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java index bea1eade..624f6819 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java @@ -217,7 +217,7 @@ public class SequentView extends CodeArea { Match va = m.getMatchings().iterator().next(); //System.out.println(va);//TODO remove for (MatchPath mp : va.values()) { - System.out.println(mp.pio()); + System.out.println("SequentView"+ mp.pio()); highlightTerm(mp.pio()); } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java index 8680487b..b81038c0 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java @@ -256,9 +256,9 @@ public class Utils { alert.setTitle("Proof Closed"); alert.setHeaderText("The proof is closed"); alert.setContentText("The proof using " + scriptName + " is closed"); - alert.setWidth(400); + alert.setWidth(500); alert.setHeight(400); - + alert.setResizable(true); /*StringWriter sw = new StringWriter(); PrintWriter pw = new PrintWriter(sw); ex.printStackTrace(pw); @@ -318,7 +318,7 @@ public class Utils { public static void intoClipboard(String s) { Map map = Collections.singletonMap(DataFormat.PLAIN_TEXT, s); Clipboard.getSystemClipboard().setContent(map); - System.err.println(s); + logger.info("Clipboard "+s); } /** diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps index 9d214290..baefca7f 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps @@ -1,5 +1,14 @@ // Please select one of the following scripts. // +script testTry(){ +cases{ + try: impLeft; + default: + __KEY_MAX_STEPS:= 100; + impRight; +} +} + script testSMT(){ smt solver='Z3'; } -- GitLab