Commit a027d3f9 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

ContinueCommand; Grammar for quantifiermatch

parent a64a5a0a
Pipeline #16864 failed with stages
in 109 minutes and 22 seconds
...@@ -22,7 +22,8 @@ sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? #sequentArrow ...@@ -22,7 +22,8 @@ sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? #sequentArrow
semiSeqPattern : termPattern (',' termPattern)*; semiSeqPattern : termPattern (',' termPattern)*;
termPattern : termPattern :
termPattern MUL termPattern #mult '(' (EXISTS|FORALL) (SID|ID) termPattern ')' #quantForm
| termPattern MUL termPattern #mult
| <assoc=right> termPattern op=(DIV|MOD) termPattern #divMod | <assoc=right> termPattern op=(DIV|MOD) termPattern #divMod
| termPattern op=(PLUS|MINUS) termPattern #plusMinus | termPattern op=(PLUS|MINUS) termPattern #plusMinus
| termPattern op=(LE|GE|LEQ|GEQ) termPattern #comparison | termPattern op=(LE|GE|LEQ|GEQ) termPattern #comparison
...@@ -53,12 +54,6 @@ bindClause : ('\\as' | ':') SID; ...@@ -53,12 +54,6 @@ bindClause : ('\\as' | ':') SID;
DONTCARE: '?' | '_' | '█'; DONTCARE: '?' | '_' | '█';
DIGITS : DIGIT+ ; DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ; fragment DIGIT : [0-9] ;
SID: '?' [_a-zA-Z0-9\\]+ ;
ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*
| 'update-application'
| 'parallel-upd'
| 'elem-update'
;
ARROW : '⇒' | '==>'; ARROW : '⇒' | '==>';
STARDONTCARE: '...' | '…'; STARDONTCARE: '...' | '…';
...@@ -78,8 +73,16 @@ OR: '|' ; ...@@ -78,8 +73,16 @@ OR: '|' ;
IMP: '->'; IMP: '->';
MOD:'%'; MOD:'%';
XOR:'^'; XOR:'^';
FORALL: '\forall' | '∀'; NOT :'!';
EXISTS: '\exists'; FORALL: '\\forall' | '∀';
EXISTS: '\\exists';
SID: '?' [_a-zA-Z0-9\\]+ ;
ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*
| 'update-application'
| 'parallel-upd'
| 'elem-update'
;
COMMENT: '//' ~[\n\r]* -> channel(HIDDEN); COMMENT: '//' ~[\n\r]* -> channel(HIDDEN);
WS: [\n\f\r\t ] -> channel(HIDDEN); WS: [\n\f\r\t ] -> channel(HIDDEN);
...@@ -54,6 +54,7 @@ public class MatcherFacadeTest { ...@@ -54,6 +54,7 @@ public class MatcherFacadeTest {
@Test @Test
public void matches() throws Exception { public void matches() throws Exception {
shouldMatchForm("\\exists int i; \\exists int j; (fint2(i, j) -> fint2(j, i))", "\\exists int i; \\exists int j; (fint2(i, j) -> fint2(j, i))");
shouldMatch("f(a)", "_"); shouldMatch("f(a)", "_");
shouldMatch("f(a)", "?X", "[{?X=f(a)}]"); shouldMatch("f(a)", "?X", "[{?X=f(a)}]");
shouldMatch("h(a,a)", "h(?X,?X)", "[{?X=a}]"); shouldMatch("h(a,a)", "h(?X,?X)", "[{?X=a}]");
......
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import java.util.Arrays;
import java.util.function.Supplier;
public class ContinueCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) {
PTreeNode<T> statePointer = dbg.getStatePointer();
if (statePointer != null) {
PTreeNode<T> stepOverPointer = statePointer.getStepOver();
if (stepOverPointer != null) {
dbg.setStatePointer(stepOverPointer);
return;
}
ASTNode[] ctx = statePointer.getContext();
//statePointer stands on the main script, we add the script itself to the context
if (statePointer.getContext().length == 0) {
ctx = Arrays.copyOf(ctx, ctx.length + 1);
ctx[ctx.length - 1] = statePointer.getStatement();
}
Supplier<Integer> currenDepth = () -> dbg.getStatePointer().getContext().length;
//Blocker.BlockPredicate predicate = new Blocker.ParentInContext(ctx);
// Blocker.SmallerContext predicate = new Blocker.SmallerContext(
// currenDepth.get(), currenDepth);
//dbg.releaseUntil(predicate);
dbg.release();
} else {
}
}
}
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import lombok.val;
public class StepIntoReverseCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) throws DebuggerException {
val statePointer = dbg.getCurrentStatePointer();
PTreeNode<T> stepBack = statePointer.getStepInvInto() != null ?
statePointer.getStepInvInto() :
statePointer.getStepInvOver();
if (stepBack == null) {
info("There is no previous state to the current one.");
}
dbg.setStatePointer(stepBack);
}
}
package edu.kit.iti.formal.psdbg.interpreter.dbg;
public class StepOverReverseCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) throws DebuggerException {
}
}
...@@ -33,6 +33,7 @@ import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; ...@@ -33,6 +33,7 @@ import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import javafx.application.Platform; import javafx.application.Platform;
import javafx.beans.binding.BooleanBinding; import javafx.beans.binding.BooleanBinding;
import javafx.collections.FXCollections; import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.concurrent.Service; import javafx.concurrent.Service;
import javafx.concurrent.Task; import javafx.concurrent.Task;
import javafx.event.ActionEvent; import javafx.event.ActionEvent;
...@@ -197,6 +198,10 @@ public class DebuggerMain implements Initializable { ...@@ -197,6 +198,10 @@ public class DebuggerMain implements Initializable {
@Override @Override
public void initialize(URL location, ResourceBundle resources) { public void initialize(URL location, ResourceBundle resources) {
init();
}
private void init() {
Events.register(this); Events.register(this);
model.setDebugMode(false); model.setDebugMode(false);
scriptController = new ScriptController(dockStation); scriptController = new ScriptController(dockStation);
...@@ -216,9 +221,16 @@ public class DebuggerMain implements Initializable { ...@@ -216,9 +221,16 @@ public class DebuggerMain implements Initializable {
proofTree.setRoot(null); proofTree.setRoot(null);
} else { } else {
proofTree.setRoot(n.root()); proofTree.setRoot(n.root());
getInspectionViewsController(). InspectionViewsController inspectionViewsController = getInspectionViewsController();
getActiveInspectionViewTab() InspectionView activeInspectionViewTab = inspectionViewsController.getActiveInspectionViewTab();
.getModel().getGoals().setAll(FACADE.getPseudoGoals()); InspectionModel model = activeInspectionViewTab.getModel();
ObservableList<GoalNode<KeyData>> goals = model.getGoals();
goals.setAll(FACADE.getPseudoGoals());
model.setSelectedGoalNodeToShow(null);
// frames / contextes zurück setzen
activeInspectionViewTab.getModel();
scriptController.getOpenScripts().keySet().forEach(ScriptArea::removeExecutionMarker);
} }
proofTree.setProof(n); proofTree.setProof(n);
} }
...@@ -295,6 +307,9 @@ public class DebuggerMain implements Initializable { ...@@ -295,6 +307,9 @@ public class DebuggerMain implements Initializable {
if (node != null) { if (node != null) {
getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt()); getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt());
scriptController.getDebugPositionHighlighter().highlight(node.getStatement()); scriptController.getDebugPositionHighlighter().highlight(node.getStatement());
} else {
getInspectionViewsController().getActiveInspectionViewTab().getFrames().getItems().clear();
scriptController.getDebugPositionHighlighter().remove();
} }
} }
...@@ -606,9 +621,9 @@ public class DebuggerMain implements Initializable { ...@@ -606,9 +621,9 @@ public class DebuggerMain implements Initializable {
public void executeToBreakpoint() { public void executeToBreakpoint() {
Set<Breakpoint> breakpoints = scriptController.getBreakpoints(); Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
if (breakpoints.size() == 0) { if (breakpoints.size() == 0) {
//System.out.println(scriptController.mainScriptProperty().get().getLineNumber()); statusBar.publishMessage("There was is no breakpoint set");
//we need to add breakpoint at end if no breakpoint exists
} }
executeScript(false); executeScript(false);
} }
...@@ -697,9 +712,55 @@ public class DebuggerMain implements Initializable { ...@@ -697,9 +712,55 @@ public class DebuggerMain implements Initializable {
} }
//endregion @FXML
public void continueAfterRun(ActionEvent event) {
LOGGER.debug("DebuggerMain.continueAfterBreakpoint");
try {
assert model.getDebuggerFramework() != null : "You should have started the prove";
model.getDebuggerFramework().execute(new ContinueCommand<>());
} catch (DebuggerException e) {
Utils.showExceptionDialog("", "", "", e);
LOGGER.error(e);
}
}
//region Actions: Menu @FXML
public void reloadProblem(ActionEvent event) {
//abort current execution();
//save old information and refresh models
File lastLoaded;
if (model.getKeyFile() != null) {
lastLoaded = model.getKeyFile();
} else {
Contract chosen = model.getChosenContract();
lastLoaded = model.getJavaFile();
}
//model.reload();
abortExecution();
handleStatePointerUI(null);
model.setStatePointer(null);
//reload getInspectionViewsController().getActiveInspectionViewTab().getModel()
InspectionModel iModel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
iModel.setHighlightedJavaLines(null);
iModel.getGoals().clear();
iModel.setSelectedGoalNodeToShow(null);
// init();
//reload File
try {
FACADE.reload(lastLoaded);
if (iModel.getGoals().size() > 0) {
iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0));
}
} catch (ProofInputException e) {
e.printStackTrace();
} catch (ProblemLoaderException e) {
e.printStackTrace();
}
}
@FXML @FXML
public void closeProgram() { public void closeProgram() {
System.exit(0); System.exit(0);
...@@ -848,7 +909,7 @@ public class DebuggerMain implements Initializable { ...@@ -848,7 +909,7 @@ public class DebuggerMain implements Initializable {
/** /**
* Perform a step back * Perform a step back
* * Does stepinto back
* @param actionEvent * @param actionEvent
*/ */
public void stepBack(ActionEvent actionEvent) { public void stepBack(ActionEvent actionEvent) {
...@@ -861,6 +922,16 @@ public class DebuggerMain implements Initializable { ...@@ -861,6 +922,16 @@ public class DebuggerMain implements Initializable {
} }
} }
public void stepIntoReverse(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMain.stepOverReverse");
try {
model.getDebuggerFramework().execute(new StepIntoReverseCommand<>());
} catch (DebuggerException e) {
Utils.showExceptionDialog("", "", "", e);
LOGGER.error(e);
}
}
public void stopDebugMode(ActionEvent actionEvent) { public void stopDebugMode(ActionEvent actionEvent) {
scriptController.getDebugPositionHighlighter().remove(); scriptController.getDebugPositionHighlighter().remove();
Button stop = (Button) actionEvent.getSource(); Button stop = (Button) actionEvent.getSource();
...@@ -1034,19 +1105,29 @@ public class DebuggerMain implements Initializable { ...@@ -1034,19 +1105,29 @@ public class DebuggerMain implements Initializable {
public void acceptUI() { public void acceptUI() {
model.getDebuggerFramework().getStatePointerListener().remove(this); model.getDebuggerFramework().getStatePointerListener().remove(this);
GoalNode<KeyData> beforeNode = original.getStateBeforeStmt().getSelectedGoalNode(); GoalNode<KeyData> beforeNode = original.getStateBeforeStmt().getSelectedGoalNode();
List<GoalNode<KeyData>> stateAfterStmt = original.getStateAfterStmt().getGoals();
ProofTree ptree = new ProofTree(); ProofTree ptree = new ProofTree();
Proof proof = beforeNode.getData().getProof(); Proof proof = beforeNode.getData().getProof();
Node pnode = beforeNode.getData().getNode(); Node pnode = beforeNode.getData().getNode();
System.out.println("pnode.serialNr() = " + pnode.serialNr());
stateAfterStmt.forEach(keyDataGoalNode -> System.out.println("keyDataGoalNode.getData().getNode().serialNr() = " + keyDataGoalNode.getData().getNode().serialNr()));
ptree.setProof(proof); ptree.setProof(proof);
ptree.setRoot(pnode); ptree.setRoot(pnode);
ptree.setDeactivateRefresh(true); ptree.setDeactivateRefresh(true);
//TODO Traversierung WICHTIG
//this is always 0 subtreegoals dies not return the subtree
//getSubtreegoals == 0
//traverse tree to closed goals -> set Sentinels
//laeves of PNode wenn aftestmt leer
//sonst nodes nodes afterstmt
Set<Node> sentinels = proof.getSubtreeGoals(pnode) Set<Node> sentinels = proof.getSubtreeGoals(pnode)
.stream() .stream()
.map(Goal::node) .map(Goal::node)
.collect(Collectors.toSet()); .collect(Collectors.toSet());
System.out.println("Sentinels: " + sentinels.isEmpty());
ptree.getSentinels().addAll(sentinels); ptree.getSentinels().addAll(sentinels);
ptree.expandRootToLeaves(); ptree.expandRootToLeaves();
//TODO set coloring of starting and end node //TODO set coloring of starting and end node
......
...@@ -58,11 +58,13 @@ public class InspectionView extends BorderPane { ...@@ -58,11 +58,13 @@ public class InspectionView extends BorderPane {
Utils.createWithFXML(this); Utils.createWithFXML(this);
frames.valueProperty().addListener((prop, o, n) -> { frames.valueProperty().addListener((prop, o, n) -> {
if (n != null) {
model.get().getGoals().setAll( model.get().getGoals().setAll(
n.getStateBeforeStmt().getGoals()); n.getStateBeforeStmt().getGoals());
model.get().setSelectedGoalNodeToShow( model.get().setSelectedGoalNodeToShow(
n.getStateBeforeStmt().getSelectedGoalNode()); n.getStateBeforeStmt().getSelectedGoalNode());
} }
}
); );
frames.setConverter(new StringConverter<PTreeNode<KeyData>>() { frames.setConverter(new StringConverter<PTreeNode<KeyData>>() {
...@@ -78,7 +80,11 @@ public class InspectionView extends BorderPane { ...@@ -78,7 +80,11 @@ public class InspectionView extends BorderPane {
}); });
model.get().selectedGoalNodeToShowProperty().addListener((o, a, b) -> { model.get().selectedGoalNodeToShowProperty().addListener((o, a, b) -> {
if (b != null) {
goalView.getSelectionModel().select(b); goalView.getSelectionModel().select(b);
} else {
goalView.getSelectionModel().clearSelection();
}
}); });
goalView.getSelectionModel().selectedItemProperty().addListener((o, a, b) -> { goalView.getSelectionModel().selectedItemProperty().addListener((o, a, b) -> {
......
...@@ -46,6 +46,7 @@ public class DebuggerMainModel { ...@@ -46,6 +46,7 @@ public class DebuggerMainModel {
*/ */
private ObservableBooleanValue executeNotPossible = new SimpleBooleanProperty();//proofTreeController.executeNotPossibleProperty().or(FACADE.readyToExecuteProperty().not()); private ObservableBooleanValue executeNotPossible = new SimpleBooleanProperty();//proofTreeController.executeNotPossibleProperty().or(FACADE.readyToExecuteProperty().not());
/** /**
* *
*/ */
...@@ -222,4 +223,6 @@ public class DebuggerMainModel { ...@@ -222,4 +223,6 @@ public class DebuggerMainModel {
public void setInterpreterState(InterpreterThreadState interpreterState) { public void setInterpreterState(InterpreterThreadState interpreterState) {
this.interpreterState.set(interpreterState); this.interpreterState.set(interpreterState);
} }
} }
script qs() { script split_from_quicksort_nice() {
autopilot_prep;
foreach{
tryclose;
}
foreach{
simp_upd;
seqPermFromSwap;
andRight;
}
cases{
case match `==> seqDef(_,_,_) = seqDef(_, _, _)`:
auto;
case match `==> \exists ...`: //hier sollten bessere branchnamen hin
instantiate var=`iv` with=`i_0`;
instantiate var=`jv` with=`j_0`;
auto;
}
}
script split_from_quicksort() {
autopilot_prep; autopilot_prep;
foreach{ foreach{
tryclose; tryclose;
...@@ -24,7 +49,7 @@ cases{ ...@@ -24,7 +49,7 @@ cases{
script quicksort() { script split_from_quicksort_rev() {
autopilot_prep; autopilot_prep;
foreach{ foreach{
tryclose; tryclose;
......
...@@ -229,6 +229,25 @@ ...@@ -229,6 +229,25 @@
</SplitMenuButton> </SplitMenuButton>
<Button onAction="#reloadProblem" disable="${controller.executeNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="REFRESH" size="24.0"/>
</graphic>
<tooltip>
<Tooltip text="Reload Problem"/>
</tooltip>
</Button>
<Button onAction="#continueAfterRun" disable="${controller.executeNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="PLAY_CIRCLE_OUTLINE" size="24.0"/>
</graphic>
<tooltip>
<Tooltip text="Continue"/>
</tooltip>
</Button>
<Button onAction="#stepInto" disable="${controller.stepNotPossible}"> <Button onAction="#stepInto" disable="${controller.stepNotPossible}">
<graphic> <graphic>
<MaterialDesignIconView glyphName="DEBUG_STEP_INTO" size="24.0"/> <MaterialDesignIconView glyphName="DEBUG_STEP_INTO" size="24.0"/>
...@@ -252,17 +271,17 @@ ...@@ -252,17 +271,17 @@
<MaterialDesignIconView glyphName="DEBUG_STEP_OVER" size="24.0" scaleX="-1"/> <MaterialDesignIconView glyphName="DEBUG_STEP_OVER" size="24.0" scaleX="-1"/>
</graphic> </graphic>
<tooltip> <tooltip>
<Tooltip text="Step Back"/> <Tooltip text="Step Over Reverse"/>
</tooltip> </tooltip>
</Button> </Button>
<Button disable="${controller.stepNotPossible}"> <Button onAction="#stepIntoReverse" disable="${controller.stepNotPossible}">
<graphic> <graphic>
<MaterialDesignIconView glyphName="DEBUG_STEP_OUT" size="24.0"/> <MaterialDesignIconView glyphName="DEBUG_STEP_OUT" size="24.0"/>
</graphic> </graphic>
<tooltip> <tooltip>
<Tooltip text="Step Out"/> <Tooltip text="Step Into Reverse"/>
</tooltip> </tooltip>
</Button> </Button>
......
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