Commit 016a8a2f authored by Sarah Grebing's avatar Sarah Grebing

Agatha Example

parent d5199937
Pipeline #14961 failed with stage
in 2 minutes and 43 seconds
......@@ -191,12 +191,12 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
@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<CaseStatement> cases = casesStatement.getCases();
for (CaseStatement aCase : cases) {
......@@ -206,12 +206,12 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
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<Void> {
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;
}
......
......@@ -128,8 +128,11 @@ public class StateGraphWrapper<T> {
} 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<T>) sucs[0];
PTreeNode nodeWithEdgeTypeSO = getNodeWithEdgeType(statePointer, EdgeTypes.STEP_OVER);
PTreeNode nodeWithEdgeTypeSF = getNodeWithEdgeType(statePointer, EdgeTypes.STATE_FLOW);
//return (PTreeNode<T>) sucs[0];
return nodeWithEdgeTypeSO;
}
//return statePointer;
......@@ -164,6 +167,13 @@ public class StateGraphWrapper<T> {
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<T> getStepBack(PTreeNode statePointer) {
Set<PTreeNode<T>> pred = this.stateGraph.predecessors(statePointer);
//if pred is empty we have reached the root
......@@ -177,6 +187,9 @@ public class StateGraphWrapper<T> {
//return statePointer;
}
private Void createNewNode(ASTNode node) {
return createNewNode(node, false);
}
......@@ -267,7 +280,9 @@ public class StateGraphWrapper<T> {
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<T> {
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<T> newStateNode = addedNodes.get(node);
//copy Current Interpreter state
State<T> 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<T> {
return null;
}
public PTreeNode<T> getNode(InterpreterExtendedState newValue) {
for (Map.Entry<ASTNode, PTreeNode<T>> 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<T> {
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<T> newStateNode = addedNodes.get(node);
//copy Current Interpreter state
State<T> 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<Void> {
@Override
......
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);
}
}
......@@ -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);
......
......@@ -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());
}
......
......@@ -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<T> {
}
public class HighlightEntryListener extends DefaultASTVisitor<Void> {
@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<T> {
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);
......
......@@ -226,7 +226,7 @@ public class ScriptArea extends CodeArea {
private void highlightNonExecutionArea() {
if (hasExecutionMarker()) {
System.out.println("getExecutionMarkerPosition() = " + getExecutionMarkerPosition());
LOGGER.debug("getExecutionMarkerPosition() = " + getExecutionMarkerPosition());
UnaryOperator<Collection<String>> styleMapper = strings -> {
......
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<GoalNode<KeyData>> currentInterpreterGoal = new SimpleObjectProperty<>(this, "currentInterpreterGoal");
private final SimpleObjectProperty<InterpreterExtendedState<KeyData>> currentExtendedState = new SimpleObjectProperty<>(this, "CurrentExtendedState");
private final MapProperty<GoalNode, Color> colorofEachGoalNodeinListView = new SimpleMapProperty<>(FXCollections.observableHashMap());
//private final StringProperty javaString = new SimpleStringProperty();
private final SetProperty<Integer> highlightedJavaLines = new SimpleSetProperty<>(FXCollections.observableSet(), "highlightedJavaLines");
......@@ -155,6 +159,18 @@ public class InspectionModel {
return isInterpreterTab;
}
public InterpreterExtendedState<KeyData> getCurrentExtendedState() {
return currentExtendedState.get();
}
public void setCurrentExtendedState(InterpreterExtendedState<KeyData> currentExtendedState) {
this.currentExtendedState.set(currentExtendedState);
}
public SimpleObjectProperty<InterpreterExtendedState<KeyData>> currentExtendedStateProperty() {
return currentExtendedState;
}
enum Mode {
LIVING, DEAD, POSTMORTEM,
}
......
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
\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
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
......@@ -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
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