Commit 9ab25960 authored by Sarah Grebing's avatar Sarah Grebing

fixed notsupported exception for non execution area highlighting and...

fixed notsupported exception for non execution area highlighting and implemnted mainscriptidentifier for prooftreecontroller
parent 559327a5
Pipeline #13294 failed with stage
in 11 seconds
...@@ -85,7 +85,7 @@ public class State<T> { ...@@ -85,7 +85,7 @@ public class State<T> {
for (GoalNode<T> goal : goals) { for (GoalNode<T> goal : goals) {
GoalNode<T> deepcopy = goal.deepCopy(); GoalNode<T> deepcopy = goal.deepCopy();
copiedGoals.add(deepcopy); copiedGoals.add(deepcopy);
if (goal.equals(selectedGoalNode)) { if (goal.equals(getSelectedGoalNode())) {
refToSelGoal = deepcopy; refToSelGoal = deepcopy;
} }
} }
......
...@@ -10,7 +10,7 @@ import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger; ...@@ -10,7 +10,7 @@ import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
import edu.kit.iti.formal.psdbg.gui.controls.*; import edu.kit.iti.formal.psdbg.gui.controls.*;
import edu.kit.iti.formal.psdbg.gui.model.Breakpoint; import edu.kit.iti.formal.psdbg.gui.model.Breakpoint;
import edu.kit.iti.formal.psdbg.gui.model.InspectionModel; import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter; import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder; import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade; import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter; import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
...@@ -190,8 +190,11 @@ public class DebuggerMain implements Initializable { ...@@ -190,8 +190,11 @@ public class DebuggerMain implements Initializable {
//System.out.println("Pos: "+newValue.getData().getNode().getNodeInfo().getActiveStatement().getPositionInfo()); //System.out.println("Pos: "+newValue.getData().getNode().getNodeInfo().getActiveStatement().getPositionInfo());
}); });
//TODO nullpointer
proofTreeController.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> { proofTreeController.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> {
scriptController.getDebugPositionHighlighter().highlight(newValue); if (newValue != null) {
scriptController.getDebugPositionHighlighter().highlight(newValue);
}
}); });
...@@ -425,12 +428,13 @@ public class DebuggerMain implements Initializable { ...@@ -425,12 +428,13 @@ public class DebuggerMain implements Initializable {
} }
/** /**
* Execute the script that with using the interpreter that is build using teh interpreterbuilder * Execute the script that with using the interpreter that is build using the interpreterbuilder
* *
* @param ib * @param ib
* @param debugMode * @param debugMode
*/ */
private void executeScript(InterpreterBuilder ib, boolean debugMode) { private void executeScript(InterpreterBuilder ib, boolean debugMode) {
Set<Breakpoint> breakpoints = scriptController.getBreakpoints(); Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
if (proofTreeController.isAlreadyExecuted()) { if (proofTreeController.isAlreadyExecuted()) {
...@@ -441,13 +445,34 @@ public class DebuggerMain implements Initializable { ...@@ -441,13 +445,34 @@ public class DebuggerMain implements Initializable {
try { try {
List<ProofScript> scripts = scriptController.getCombinedAST(); List<ProofScript> scripts = scriptController.getCombinedAST();
int n = 0;
if (scriptController.getMainScript() == null) {
MainScriptIdentifier msi = new MainScriptIdentifier();
msi.setLineNumber(scripts.get(0).getStartPosition().getLineNumber());
msi.setScriptName(scripts.get(0).getName());
msi.setSourceName(scripts.get(0).getRuleContext().getStart().getInputStream().getSourceName());
msi.setScriptArea(scriptController.findEditor(new File(scripts.get(0).getRuleContext().getStart().getInputStream().getSourceName())));
scriptController.setMainScript(msi);
n = 0;
} else {
for (int i = 0; i < scripts.size(); i++) {
ProofScript proofScript = scripts.get(i);
if (proofScript.getName().equals(scriptController.getMainScript().getScriptName())) {
n = i;
break;
}
}
}
statusBar.publishMessage("Creating new Interpreter instance ..."); statusBar.publishMessage("Creating new Interpreter instance ...");
ib.setScripts(scripts); ib.setScripts(scripts);
KeyInterpreter currentInterpreter = ib.build(); KeyInterpreter currentInterpreter = ib.build();
proofTreeController.setCurrentInterpreter(currentInterpreter); proofTreeController.setCurrentInterpreter(currentInterpreter);
proofTreeController.setMainScript(scripts.get(0)); proofTreeController.setMainScript(scripts.get(n));
statusBar.publishMessage("Executing script " + scripts.get(0).getName());
statusBar.publishMessage("Executing script " + scripts.get(n).getName());
proofTreeController.executeScript(this.debugMode.get(), statusBar, breakpoints); proofTreeController.executeScript(this.debugMode.get(), statusBar, breakpoints);
//highlight signature of main script //highlight signature of main script
//scriptController.setDebugMark(scripts.get(0).getStartPosition().getLineNumber()); //scriptController.setDebugMark(scripts.get(0).getStartPosition().getLineNumber());
......
...@@ -92,24 +92,33 @@ public class ProofTreeController { ...@@ -92,24 +92,33 @@ public class ProofTreeController {
private PTreeNode<KeyData> statePointer = null; private PTreeNode<KeyData> statePointer = null;
/** /**
* Teh mainscipt that is executed * The mainscipt that is executed
*/ */
private ProofScript mainScript; private SimpleObjectProperty<ProofScript> mainScript = new SimpleObjectProperty<>();
/** /**
* Add a change listener for the stategraph, whenever a new node is added it receives an event * Add a change listener for the stategraph, whenever a new node is added it receives an event
*/ */
private GraphChangedListener graphChangedListener = nodeAddedEvent -> { private GraphChangedListener graphChangedListener = nodeAddedEvent -> {
if (statePointer.equals(nodeAddedEvent.getLastPointer())) { //if (statePointer.equals(nodeAddedEvent.getLastPointer())) {
//set value of newly computed node //set value of newly computed node
nextComputedNode.setValue(nodeAddedEvent.getAddedNode()); nextComputedNode.setValue(nodeAddedEvent.getAddedNode());
//setNewState(this.statePointer.getState());
Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScriptstmt())); Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScriptstmt()));
} //}
}; };
public ProofScript getMainScript() {
return mainScript.get();
}
public void setMainScript(ProofScript mainScript) {
this.mainScript.set(mainScript);
}
public SimpleObjectProperty<ProofScript> mainScriptProperty() {
return mainScript;
}
/** /**
* Create a new ProofTreeController * Create a new ProofTreeController
* and bind properties * and bind properties
...@@ -258,12 +267,12 @@ public class ProofTreeController { ...@@ -258,12 +267,12 @@ public class ProofTreeController {
} else { } else {
statusBar.setText("Starting in debug mode for script " + mainScript.getName()); statusBar.setText("Starting in debug mode for script " + mainScript.getName());
statusBar.indicateProgress(); statusBar.indicateProgress();
setCurrentHighlightNode(mainScript.getSignature()); setCurrentHighlightNode(mainScript.get());
//build CFG //build CFG
buildControlFlowGraph(mainScript); buildControlFlowGraph(mainScript.get());
//build StateGraph //build StateGraph
this.stateGraphWrapper = new StateGraphWrapper(currentInterpreter, this.mainScript, this.controlFlowGraphVisitor); this.stateGraphWrapper = new StateGraphWrapper(currentInterpreter, mainScript.get(), this.controlFlowGraphVisitor);
this.stateGraphWrapper.install(currentInterpreter); this.stateGraphWrapper.install(currentInterpreter);
this.stateGraphWrapper.addChangeListener(graphChangedListener); this.stateGraphWrapper.addChangeListener(graphChangedListener);
...@@ -277,7 +286,8 @@ public class ProofTreeController { ...@@ -277,7 +286,8 @@ public class ProofTreeController {
interpreterService.reset(); interpreterService.reset();
} }
interpreterService.interpreterProperty().set(currentInterpreter); interpreterService.interpreterProperty().set(currentInterpreter);
interpreterService.mainScriptProperty().set(mainScript);
interpreterService.mainScriptProperty().set(mainScript.get());
interpreterService.start(); interpreterService.start();
interpreterService.setOnSucceeded(event -> { interpreterService.setOnSucceeded(event -> {
statusBar.setText("Executed script until end of script."); statusBar.setText("Executed script until end of script.");
...@@ -298,6 +308,7 @@ public class ProofTreeController { ...@@ -298,6 +308,7 @@ public class ProofTreeController {
private void buildControlFlowGraph(ProofScript mainScript) { private void buildControlFlowGraph(ProofScript mainScript) {
this.controlFlowGraphVisitor = new ControlFlowVisitor(currentInterpreter.getFunctionLookup()); this.controlFlowGraphVisitor = new ControlFlowVisitor(currentInterpreter.getFunctionLookup());
mainScript.accept(controlFlowGraphVisitor); mainScript.accept(controlFlowGraphVisitor);
this.setMainScript(mainScript);
System.out.println("CFG\n" + controlFlowGraphVisitor.asdot()); System.out.println("CFG\n" + controlFlowGraphVisitor.asdot());
} }
...@@ -335,10 +346,10 @@ public class ProofTreeController { ...@@ -335,10 +346,10 @@ public class ProofTreeController {
this.currentInterpreter = currentInterpreter; this.currentInterpreter = currentInterpreter;
} }
public void setMainScript(ProofScript mainScript) { /* public void setMainScript(ProofScript mainScript) {
this.mainScript = mainScript; this.mainScript = mainScript;
} }*/
public StateGraphWrapper getStateVisitor() { public StateGraphWrapper getStateVisitor() {
return this.stateGraphWrapper; return this.stateGraphWrapper;
......
...@@ -54,6 +54,7 @@ import java.time.Duration; ...@@ -54,6 +54,7 @@ import java.time.Duration;
import java.util.*; import java.util.*;
import java.util.function.Consumer; import java.util.function.Consumer;
import java.util.function.IntFunction; import java.util.function.IntFunction;
import java.util.function.UnaryOperator;
/** /**
* ScriptArea is the {@link CodeArea} for writing Proof Scripts. * ScriptArea is the {@link CodeArea} for writing Proof Scripts.
...@@ -225,10 +226,42 @@ public class ScriptArea extends CodeArea { ...@@ -225,10 +226,42 @@ public class ScriptArea extends CodeArea {
private void highlightNonExecutionArea() { private void highlightNonExecutionArea() {
if (hasExecutionMarker()) { if (hasExecutionMarker()) {
getStyleSpans(0, getExecutionMarkerPosition()).forEach(span -> { System.out.println("getExecutionMarkerPosition() = " + getExecutionMarkerPosition());
span.getStyle().add("NON_EXE_AREA");
/* getStyleSpans(0, getExecutionMarkerPosition()).stream()
.map(span -> {
Collection<String> style = span.getStyle();
if (style.isEmpty()) {
Collections.singleton("NON_EXE_AREA");
} else {
style.add("NON_EXE_AREA");
}
return style;
});*/
UnaryOperator<Collection<String>> styleMapper = strings -> {
if (strings.isEmpty()) {
return Collections.singleton("NON_EXE_AREA");
} else {
Collection res = strings;
res.add("NON_EXE_AREA");
return res;
}
};
setStyleSpans(0, getStyleSpans(0, getExecutionMarkerPosition()).mapStyles(styleMapper));
/* getStyleSpans(0, getExecutionMarkerPosition()).forEach(span -> {
Collection<String> style = span.getStyle();
if (style.isEmpty()) {
style.add("NON_EXE_AREA");
//setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA"));
} else {
style.add("NON_EXE_AREA");
}
}); });
//setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA")); */
} }
} }
...@@ -305,7 +338,7 @@ public class ScriptArea extends CodeArea { ...@@ -305,7 +338,7 @@ public class ScriptArea extends CodeArea {
public Collection<? extends Breakpoint> getBreakpoints() { public Collection<? extends Breakpoint> getBreakpoints() {
List<Breakpoint> list = new ArrayList<>(); List<Breakpoint> list = new ArrayList<>();
int line = 0; int line = 1;
for (GutterAnnotation s : gutter.lineAnnotations) { for (GutterAnnotation s : gutter.lineAnnotations) {
if (s.isBreakpoint()) { if (s.isBreakpoint()) {
Breakpoint b = new Breakpoint(filePath.get(), line); Breakpoint b = new Breakpoint(filePath.get(), line);
......
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