From 016a8a2f77b5c8c1c4722b7722d434a57e2d8956 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Fri, 27 Oct 2017 12:36:38 +0200 Subject: [PATCH] Agatha Example --- .../graphs/ControlFlowVisitor.java | 36 +++---- .../interpreter/graphs/StateGraphWrapper.java | 102 ++++++++++++------ .../psdbg/examples/agatha/AgathaExample.java | 11 ++ .../psdbg/gui/controller/DebuggerMain.java | 1 + .../gui/controller/ProofTreeController.java | 9 +- .../gui/controls/ASTNodeHiglightListener.java | 16 +-- .../formal/psdbg/gui/controls/ScriptArea.java | 2 +- .../psdbg/gui/model/InspectionModel.java | 16 +++ .../edu.kit.iti.formal.psdbg.examples.Example | 3 +- .../formal/psdbg/examples/agatha/problem.key | 85 +++++++++++++++ .../formal/psdbg/examples/agatha/script.kps | 28 +++++ ui/src/main/resources/log4j2.properties | 4 +- 12 files changed, 241 insertions(+), 72 deletions(-) create mode 100644 ui/src/main/java/edu/kit/iti/formal/psdbg/examples/agatha/AgathaExample.java create mode 100644 ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/problem.key create mode 100644 ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/ControlFlowVisitor.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/ControlFlowVisitor.java index fd6fa58a..849ebdcb 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/ControlFlowVisitor.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/ControlFlowVisitor.java @@ -191,12 +191,12 @@ public class ControlFlowVisitor extends DefaultASTVisitor { @Override public Void visit(CasesStatement casesStatement) { - ControlFlowNode currentNode = new ControlFlowNode(casesStatement); - mappingOfNodes.put(casesStatement, currentNode); - graph.addNode(currentNode); - //System.out.println("\n" + currentNode + "\n"); - graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); - graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK); + ControlFlowNode casesNode = new ControlFlowNode(casesStatement); + mappingOfNodes.put(casesStatement, casesNode); + graph.addNode(casesNode); + //System.out.println("\n" + casesNode + "\n"); + graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_OVER); + graph.putEdgeValue(casesNode, lastNode, EdgeTypes.STEP_BACK); List cases = casesStatement.getCases(); for (CaseStatement aCase : cases) { @@ -206,12 +206,12 @@ public class ControlFlowVisitor extends DefaultASTVisitor { ControlFlowNode caseNode = new ControlFlowNode(aCase); mappingOfNodes.put(aCase, caseNode); graph.addNode(caseNode); - //System.out.println("\n" + caseNode + "\n"); - graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right? - graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK); + //TODO rethink + graph.putEdgeValue(casesNode, caseNode, EdgeTypes.STEP_INTO); //??is this right? + graph.putEdgeValue(caseNode, casesNode, EdgeTypes.STEP_BACK); lastNode = caseNode; aCase.getBody().accept(this); - graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); + graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_RETURN); // } } //casesStatement.getDefaultCase() @@ -220,25 +220,25 @@ public class ControlFlowVisitor extends DefaultASTVisitor { ControlFlowNode caseNode = new ControlFlowNode(defCase); mappingOfNodes.put(defCase, caseNode); graph.addNode(caseNode); - //System.out.println("\n" + caseNode + "\n"); - graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right? - graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK); +//TODO rethink + graph.putEdgeValue(casesNode, caseNode, EdgeTypes.STEP_INTO); //??is this right? + graph.putEdgeValue(caseNode, casesNode, EdgeTypes.STEP_BACK); lastNode = caseNode; defCase.getBody().accept(this); - graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); + graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_RETURN); /*Statements defaultCase = defCase.getBody(); ControlFlowNode caseNode = new ControlFlowNode(defaultCase); mappingOfNodes.put(defaultCase, caseNode); graph.addNode(caseNode); //System.out.println("\n" + caseNode + "\n"); - graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right? - graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK); + graph.putEdgeValue(casesNode, caseNode, EdgeTypes.STEP_OVER); //??is this right? + graph.putEdgeValue(caseNode, casesNode, EdgeTypes.STEP_BACK); lastNode = caseNode; defaultCase.accept(this); - graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);*/ + graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_RETURN);*/ } - lastNode = currentNode; + lastNode = casesNode; return null; } diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java index ca15d926..330d511f 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java @@ -128,8 +128,11 @@ public class StateGraphWrapper { } else { //if there are successors we want those which are connetced with State-Flow Object[] sucs = successors.toArray(); - getNodeWithEdgeType(statePointer, EdgeTypes.STATE_FLOW); - return (PTreeNode) sucs[0]; + PTreeNode nodeWithEdgeTypeSO = getNodeWithEdgeType(statePointer, EdgeTypes.STEP_OVER); + PTreeNode nodeWithEdgeTypeSF = getNodeWithEdgeType(statePointer, EdgeTypes.STATE_FLOW); + + //return (PTreeNode) sucs[0]; + return nodeWithEdgeTypeSO; } //return statePointer; @@ -164,6 +167,13 @@ public class StateGraphWrapper { return null; } + /** + * Return the predecessor node from the statepointer if it exists, the statepointer itself is not-existing, + * because in this case we have reached the end of the graph + * + * @param statePointer + * @return + */ public PTreeNode getStepBack(PTreeNode statePointer) { Set> pred = this.stateGraph.predecessors(statePointer); //if pred is empty we have reached the root @@ -177,6 +187,9 @@ public class StateGraphWrapper { //return statePointer; } + + + private Void createNewNode(ASTNode node) { return createNewNode(node, false); } @@ -267,7 +280,9 @@ public class StateGraphWrapper { newStateNode.setExtendedState(extState); stateGraph.addNode(newStateNode); + stateGraph.putEdgeValue(lastNode, newStateNode, EdgeTypes.STATE_FLOW); + //inform listeners about a new node in the graph fireNodeAdded(new NodeAddedEvent(lastNode, newStateNode)); addedNodes.put(node, newStateNode); @@ -275,6 +290,47 @@ public class StateGraphWrapper { return null; } + /** + * Add a new state to an existing PTreeNode + * + * @param node + * @param fireStateAdded + * @return + */ + private Void addState(ASTNode node, boolean fireStateAdded) { + LOGGER.info("Adding a new state for statement {}@{}", node.getNodeName(), node.getStartPosition()); + //get node from addedNodes Map + PTreeNode newStateNode = addedNodes.get(node); + //copy Current Interpreter state + State currentState = currentInterpreter.getCurrentState().copy(); + //set the state + if (node != this.root.get().getScriptstmt()) { + newStateNode.setState(currentState); + newStateNode.getExtendedState().setStateAfterStmt(currentState); + if (newStateNode.getContext().peek().equals(node)) { + newStateNode.getContext().pop(); + } + } else { + // newStateNode.setState(currentState); + newStateNode.getExtendedState().setStateAfterStmt(currentState); + if (newStateNode.getContext().peek().equals(node)) { + newStateNode.getContext().pop(); + } + } + if (fireStateAdded) { + fireStateAdded(new StateAddedEvent(newStateNode, currentState, newStateNode.getExtendedState())); + } + LOGGER.debug("Extended state for {} updated with {} \n", node.getStartPosition(), newStateNode.getExtendedState().toString()); + return null; + } + + private void fireStateAdded(StateAddedEvent stateAddedEvent) { + changeListeners.forEach(list -> Platform.runLater(() -> { + list.graphChanged(stateAddedEvent); + // LOGGER.debug("New StateGraphChange " + this.asdot()); + })); + } + private void fireNodeAdded(NodeAddedEvent nodeAddedEvent) { changeListeners.forEach(list -> Platform.runLater(() -> { list.graphChanged(nodeAddedEvent); @@ -328,6 +384,16 @@ public class StateGraphWrapper { return null; } + public PTreeNode getNode(InterpreterExtendedState newValue) { + for (Map.Entry> next : addedNodes.entrySet()) { + PTreeNode value = next.getValue(); + if (value.getExtendedState().equals(newValue)) { + return value; + } + } + return null; + } + /** * Helper for debugging * @return @@ -372,39 +438,7 @@ public class StateGraphWrapper { return sb.toString(); } - private Void addState(ASTNode node, boolean fireStateAdded) { - LOGGER.info("Adding a new state for statement {}@{}", node.getNodeName(), node.getStartPosition()); - //get node from addedNodes Map - PTreeNode newStateNode = addedNodes.get(node); - //copy Current Interpreter state - State currentState = currentInterpreter.getCurrentState().copy(); - //set the state - if (node != this.root.get().getScriptstmt()) { - newStateNode.setState(currentState); - newStateNode.getExtendedState().setStateAfterStmt(currentState); - if (newStateNode.getContext().peek().equals(node)) { - newStateNode.getContext().pop(); - } - } else { - // newStateNode.setState(currentState); - newStateNode.getExtendedState().setStateAfterStmt(currentState); - if (newStateNode.getContext().peek().equals(node)) { - newStateNode.getContext().pop(); - } - } - if (fireStateAdded) { - fireStateAdded(new StateAddedEvent(newStateNode, currentState, newStateNode.getExtendedState())); - } - LOGGER.debug("Extended state for {} updated with {} \n", node.getStartPosition(), newStateNode.getExtendedState().toString()); - return null; - } - private void fireStateAdded(StateAddedEvent stateAddedEvent) { - changeListeners.forEach(list -> Platform.runLater(() -> { - list.graphChanged(stateAddedEvent); - // LOGGER.debug("New StateGraphChange " + this.asdot()); - })); - } private class EntryListener extends DefaultASTVisitor { @Override diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/agatha/AgathaExample.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/agatha/AgathaExample.java new file mode 100644 index 00000000..f33264e8 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/agatha/AgathaExample.java @@ -0,0 +1,11 @@ +package edu.kit.iti.formal.psdbg.examples.agatha; + +import edu.kit.iti.formal.psdbg.examples.Example; + +public class AgathaExample extends Example { + public AgathaExample() { + setName("Agatha"); + defaultInit(getClass()); + System.out.println(this); + } +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index a85f7176..579bdf43 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java @@ -186,6 +186,7 @@ public class DebuggerMain implements Initializable { proofTreeController.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> { + imodel.setCurrentInterpreterGoal(newValue); //also update the selected to be shown imodel.setSelectedGoalNodeToShow(newValue); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java index 183b4541..0b7426af 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java @@ -254,7 +254,7 @@ public class ProofTreeController { //if nextnode is null ask interpreter to execute next statement and compute next state if (nextNode != null) { - //setCurrentHighlightNode(nextNode.getScriptstmt()); + setCurrentHighlightNode(nextNode.getScriptstmt()); } if (nextNode != null && nextNode.getExtendedState().getStateAfterStmt() != null) { @@ -290,7 +290,8 @@ public class ProofTreeController { if (current != null) { this.statePointer = stateGraphWrapper.getStepBack(current); if (this.statePointer != null) { - setNewState(statePointer.getState()); + setNewState(statePointer.getExtendedState().getStateBeforeStmt()); + setCurrentHighlightNode(statePointer.getScriptstmt()); } else { this.statePointer = current; } @@ -298,6 +299,8 @@ public class ProofTreeController { } public PTreeNode stepInto() { + PTreeNode current = this.statePointer; + return null; } @@ -390,7 +393,7 @@ public class ProofTreeController { this.controlFlowGraphVisitor = new ControlFlowVisitor(currentInterpreter.getFunctionLookup()); mainScript.accept(controlFlowGraphVisitor); this.setMainScript(mainScript); - LOGGER.debug("CFG\n" + controlFlowGraphVisitor.asdot()); + LOGGER.info("CFG\n" + controlFlowGraphVisitor.asdot()); } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ASTNodeHiglightListener.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ASTNodeHiglightListener.java index e368c67a..6145311b 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ASTNodeHiglightListener.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ASTNodeHiglightListener.java @@ -3,8 +3,7 @@ package edu.kit.iti.formal.psdbg.gui.controls; import edu.kit.iti.formal.psdbg.interpreter.Interpreter; import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor; 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.ProofScript; +import edu.kit.iti.formal.psdbg.parser.ast.Parameters; import edu.kit.iti.formal.psdbg.parser.ast.Statements; import javafx.application.Platform; import javafx.beans.property.SimpleObjectProperty; @@ -54,15 +53,9 @@ public class ASTNodeHiglightListener { } public class HighlightEntryListener extends DefaultASTVisitor { - - @Override - public Void visit(ProofScript proofScript) { - return defaultVisit(proofScript); - } - @Override - public Void visit(CallStatement proofScript) { - return defaultVisit(proofScript); + public Void visit(Parameters parameters) { + return null; } @Override @@ -74,9 +67,6 @@ public class ASTNodeHiglightListener { public Void defaultVisit(ASTNode node) { if (node != null) { lastHighlightedNode = node; - System.out.println("nodeInHighlighter = " + node); - System.out.println("lastHighlightedNode = " + lastHighlightedNode); - Platform.runLater(() -> { currentHighlightNode.setValue(lastHighlightedNode); 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 6e209a9f..38bbd88b 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 @@ -226,7 +226,7 @@ public class ScriptArea extends CodeArea { private void highlightNonExecutionArea() { if (hasExecutionMarker()) { - System.out.println("getExecutionMarkerPosition() = " + getExecutionMarkerPosition()); + LOGGER.debug("getExecutionMarkerPosition() = " + getExecutionMarkerPosition()); UnaryOperator> styleMapper = strings -> { diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java index 66a775c8..33ed56f8 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java @@ -1,6 +1,7 @@ package edu.kit.iti.formal.psdbg.gui.model; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; +import edu.kit.iti.formal.psdbg.interpreter.data.InterpreterExtendedState; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; import javafx.beans.property.*; @@ -26,6 +27,9 @@ public class InspectionModel { //aktuell im Interpreter aktives Goal private final ObjectProperty> currentInterpreterGoal = new SimpleObjectProperty<>(this, "currentInterpreterGoal"); + + private final SimpleObjectProperty> currentExtendedState = new SimpleObjectProperty<>(this, "CurrentExtendedState"); + private final MapProperty colorofEachGoalNodeinListView = new SimpleMapProperty<>(FXCollections.observableHashMap()); //private final StringProperty javaString = new SimpleStringProperty(); private final SetProperty highlightedJavaLines = new SimpleSetProperty<>(FXCollections.observableSet(), "highlightedJavaLines"); @@ -155,6 +159,18 @@ public class InspectionModel { return isInterpreterTab; } + + public InterpreterExtendedState getCurrentExtendedState() { + return currentExtendedState.get(); + } + + public void setCurrentExtendedState(InterpreterExtendedState currentExtendedState) { + this.currentExtendedState.set(currentExtendedState); + } + + public SimpleObjectProperty> currentExtendedStateProperty() { + return currentExtendedState; + } enum Mode { LIVING, DEAD, POSTMORTEM, } diff --git a/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example b/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example index ad1b76ec..3f6ef46f 100644 --- a/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example +++ b/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example @@ -1,4 +1,5 @@ edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample -edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample \ No newline at end of file +edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample +edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample \ No newline at end of file diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/problem.key b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/problem.key new file mode 100644 index 00000000..80a712b6 --- /dev/null +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/problem.key @@ -0,0 +1,85 @@ +\profile "Java Profile"; + +\settings { +"#Proof-Settings-Config-File +#Wed Sep 27 23:52:00 CEST 2017 +[StrategyProperty]VBT_PHASE=VBT_SYM_EX +[SMTSettings]useUninterpretedMultiplication=true +[SMTSettings]SelectedTaclets= +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_COMPLETION +[SMTSettings]instantiateHierarchyAssumptions=true +[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF +[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON +[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT +[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE +[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF +[Strategy]Timeout=-1 +[Strategy]MaximumNumberOfAutomaticApplications=10000 +[SMTSettings]integersMaximum=2147483645 +[Choice]DefaultChoices=assertions-assertions\\:on , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , joinGenerateIsWeakeningGoal-joinGenerateIsWeakeningGoal\\:off , debug-debug\\:off +[SMTSettings]useConstantsForBigOrSmallIntegers=true +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON +[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE +[SMTSettings]maxGenericSorts=2 +[SMTSettings]integersMinimum=-2147483645 +[SMTSettings]invariantForall=false +[SMTSettings]UseBuiltUniqueness=false +[SMTSettings]explicitTypeHierarchy=false +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +" +} + +\sorts { + S; +} + +\functions { + S agatha; + S butler; + S charles; +} + +\predicates { + lives(S); + hates(S, S); + killed(S, S); + richer(S, S); + equal(S, S); +} + + +\problem { + \exists S z7; (lives(z7) & killed(z7, agatha)) + & lives(agatha) + & lives(butler) + & lives(charles) + & \forall S z8; + ( lives(z8) + -> z8 = agatha | (z8 = butler | z8 = charles)) + & \forall S z9; + \forall S z0; (killed(z9, z0) -> hates(z9, z0)) + & \forall S w1; + \forall S w2; + (killed(w1, w2) -> !richer(w1, w2)) + & \forall S w3; + (hates(agatha, w3) -> !hates(charles, w3)) + & \forall S w4; (!w4 = butler -> hates(agatha, w4)) + & \forall S w5; + (!richer(w5, agatha) -> hates(butler, w5)) + & \forall S w6; + (hates(agatha, w6) -> hates(butler, w6)) + & \forall S w7; \exists S w8; !hates(w7, w8) + & !agatha = butler +-> killed(agatha, agatha) + +} \ No newline at end of file diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps new file mode 100644 index 00000000..95d9f6db --- /dev/null +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps @@ -0,0 +1,28 @@ +script agascript() { +impRight; +andLeft; +notLeft; + +andLeft; +andLeft; +andLeft; +andLeft; +andLeft; +andLeft; +andLeft; +andLeft; +andLeft; +andLeft; +andLeft; + +exLeft; +andLeft; +eqSymm formula = `agatha = butler`; +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))`; +} \ No newline at end of file diff --git a/ui/src/main/resources/log4j2.properties b/ui/src/main/resources/log4j2.properties index 562f116a..b96d1655 100644 --- a/ui/src/main/resources/log4j2.properties +++ b/ui/src/main/resources/log4j2.properties @@ -19,5 +19,5 @@ logger.file.level = debug logger.file.appenderRefs = file logger.file.appenderRef.file.ref = LOGFILE rootLogger.level=info -rootLogger.appenderRefs=file -rootLogger.appenderRef.stdout.ref=LOGFILE \ No newline at end of file +rootLogger.appenderRefs=stdout +rootLogger.appenderRef.stdout.ref=STDOUT \ No newline at end of file -- 2.26.2