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 f1805d9fb24b766430cc46679b0ea38767357744..2547f8fab23c94e1d937e71318b3fcd8a4a1ea53 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 2c27a55420908ad5f7b2ee2833bd8971feae187f..862d38615eec8173013779e8b5d12e27f4f1d0fc 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 54e767070f654a1a7ae590e11624c21722a5bb4f..d7b734ac6292514a355222e51bb88518efdca916 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 62ea6b2f4907d4ebc28d577129e8be056be0a6a0..9b721a89c720d294b3d04b55eaf811f15fa61fda 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 bea1eade9a2ecf82b7723127a2dfc3084aae3016..624f68199adc827664c5250be1b3088b7bb75de0 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 8680487b645fbed8d825fa425ae5abbe90fb1443..b81038c0bdd6af8b172fd11691aa002b89d29e82 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 9d2142907d4ac082c731ab105986cfd76702cbd0..baefca7f31dfc9a72fb11ea8edf4de5ce2dd3e48 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'; }