Commit 73c88fff authored by Sarah Grebing's avatar Sarah Grebing

First footsteps towards interactive mode

parent 2bb39b6d
Pipeline #15248 passed with stages
in 10 minutes and 30 seconds
...@@ -127,6 +127,9 @@ public class DebuggerMain implements Initializable { ...@@ -127,6 +127,9 @@ public class DebuggerMain implements Initializable {
@FXML @FXML
private CheckMenuItem miProofTree; private CheckMenuItem miProofTree;
@FXML
private Button btnIM;
private JavaArea javaArea = new JavaArea(); private JavaArea javaArea = new JavaArea();
private DockNode javaAreaDock = new DockNode(javaArea, "Java Source", private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
...@@ -148,6 +151,8 @@ public class DebuggerMain implements Initializable { ...@@ -148,6 +151,8 @@ public class DebuggerMain implements Initializable {
private DockNode commandHelpDock = new DockNode(commandHelp, "DebuggerCommand Help"); private DockNode commandHelpDock = new DockNode(commandHelp, "DebuggerCommand Help");
private InteractiveModeController interactiveModeController;
@FXML @FXML
private Menu examplesMenu; private Menu examplesMenu;
...@@ -193,6 +198,7 @@ public class DebuggerMain implements Initializable { ...@@ -193,6 +198,7 @@ public class DebuggerMain implements Initializable {
Events.register(this); Events.register(this);
model.setDebugMode(false); model.setDebugMode(false);
scriptController = new ScriptController(dockStation); scriptController = new ScriptController(dockStation);
interactiveModeController = new InteractiveModeController(scriptController);
inspectionViewsController = new InspectionViewsController(dockStation); inspectionViewsController = new InspectionViewsController(dockStation);
activeInspectorDock = inspectionViewsController.getActiveInterpreterTabDock(); activeInspectorDock = inspectionViewsController.getActiveInterpreterTabDock();
//register the welcome dock in the center //register the welcome dock in the center
...@@ -493,10 +499,12 @@ public class DebuggerMain implements Initializable { ...@@ -493,10 +499,12 @@ public class DebuggerMain implements Initializable {
Platform.runLater(() -> { Platform.runLater(() -> {
scriptController.getDebugPositionHighlighter().remove(); scriptController.getDebugPositionHighlighter().remove();
statusBar.publishSuccessMessage("Interpreter finished."); statusBar.publishSuccessMessage("Interpreter finished.");
btnIM.setDisable(false);
assert model.getDebuggerFramework() != null; assert model.getDebuggerFramework() != null;
PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer(); PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
State<KeyData> lastState = statePointer.getStateAfterStmt(); State<KeyData> lastState = statePointer.getStateAfterStmt();
getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState); getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState);
}); });
} }
...@@ -834,10 +842,27 @@ public class DebuggerMain implements Initializable { ...@@ -834,10 +842,27 @@ public class DebuggerMain implements Initializable {
stop.setText("Reload"); stop.setText("Reload");
} }
/* public void handle(Events.TacletApplicationEvent tap){
TacletApp app = tap.getApp();
Goal currentGoal = tap.getCurrentGoal();
ImmutableList<Goal> apply = currentGoal.apply(app);
}*/
public void newScript(ActionEvent actionEvent) { public void newScript(ActionEvent actionEvent) {
scriptController.newScript(); scriptController.newScript();
} }
@FXML
public void interactiveMode(ActionEvent actionEvent) {
interactiveModeController.setActivated(true);
interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel());
}
@FXML @FXML
public void showWelcomeDock(ActionEvent actionEvent) { public void showWelcomeDock(ActionEvent actionEvent) {
if (!welcomePaneDock.isDocked() && !welcomePaneDock.isFloating()) { if (!welcomePaneDock.isDocked() && !welcomePaneDock.isFloating()) {
......
...@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.gui.controller; ...@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.gui.controller;
import com.google.common.eventbus.EventBus; import com.google.common.eventbus.EventBus;
import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.TacletApp;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea; import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea;
...@@ -47,8 +48,11 @@ public class Events { ...@@ -47,8 +48,11 @@ public class Events {
@RequiredArgsConstructor @RequiredArgsConstructor
public static class TacletApplicationEvent { public static class TacletApplicationEvent {
private final TacletApp app; private final TacletApp app;
private final PosInOccurrence pio; private final PosInOccurrence pio;
private final Goal currentGoal;
} }
@Data @Data
......
package edu.kit.iti.formal.psdbg.gui.controller; package edu.kit.iti.formal.psdbg.gui.controller;
import com.google.common.eventbus.Subscribe; import com.google.common.eventbus.Subscribe;
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.logic.SequentFormula; import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.LabelFactory; import edu.kit.iti.formal.psdbg.LabelFactory;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptController;
import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
import edu.kit.iti.formal.psdbg.parser.PrettyPrinter; import edu.kit.iti.formal.psdbg.parser.PrettyPrinter;
import edu.kit.iti.formal.psdbg.parser.ast.*; import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.beans.property.BooleanProperty; import javafx.beans.property.BooleanProperty;
import javafx.beans.property.SimpleBooleanProperty; import javafx.beans.property.SimpleBooleanProperty;
import javafx.collections.ObservableList;
import lombok.Getter; import lombok.Getter;
import lombok.RequiredArgsConstructor;
import lombok.Setter; import lombok.Setter;
import lombok.val; import lombok.val;
import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import java.util.HashMap; import java.util.HashMap;
import java.util.List;
import java.util.Map; import java.util.Map;
import java.util.stream.Collectors;
@Getter @Getter
@Setter @Setter
@RequiredArgsConstructor
public class InteractiveModeController { public class InteractiveModeController {
private static final Logger LOGGER = LogManager.getLogger(InteractiveModeController.class); private static final Logger LOGGER = LogManager.getLogger(InteractiveModeController.class);
...@@ -26,13 +46,22 @@ public class InteractiveModeController { ...@@ -26,13 +46,22 @@ public class InteractiveModeController {
private BooleanProperty activated = new SimpleBooleanProperty(); private BooleanProperty activated = new SimpleBooleanProperty();
private final ScriptController scriptController;
public InteractiveModeController() { private ScriptArea scriptArea;
}
private InspectionModel model;
public void start() {
public void start(Proof currentProof, InspectionModel model) {
Events.register(this); Events.register(this);
cases.clear(); cases.clear();
currentProof.getSubtreeGoals(currentProof.root()).forEach(goal -> {
cases.put(goal.node(), new Statements());
});
this.scriptArea = scriptController.newScript();
this.model = model;
} }
public void stop() { public void stop() {
...@@ -45,22 +74,30 @@ public class InteractiveModeController { ...@@ -45,22 +74,30 @@ public class InteractiveModeController {
public void handle(Events.TacletApplicationEvent tap) { public void handle(Events.TacletApplicationEvent tap) {
LOGGER.debug("Handling {}", tap); LOGGER.debug("Handling {}", tap);
String tapName = tap.getApp().taclet().displayName(); String tapName = tap.getApp().taclet().displayName();
Goal g = tap.getCurrentGoal();
SequentFormula seqForm = tap.getPio().sequentFormula(); SequentFormula seqForm = tap.getPio().sequentFormula();
//transform term to parsable string representation //transform term to parsable string representation
String term = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(seqForm.formula()); String term = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(seqForm.formula());
Parameters params = new Parameters(); Parameters params = new Parameters();
params.put(new Variable("formula"), new TermLiteral(term)); params.put(new Variable("formula"), new TermLiteral(term));
VariableAssignment va = new VariableAssignment(null);
CallStatement call = new CallStatement(tapName, params); CallStatement call = new CallStatement(tapName, params);
// Insert into the right cases // Insert into the right cases
Node currentNode = null; Node currentNode = g.node();
cases.get(findRoot(currentNode)).add(call); cases.get(findRoot(currentNode)).add(call);
// How to Play this on the Proof? // How to Play this on the Proof?
// How to Build a new StatePointer? Is it still possible? // How to Build a new StatePointer? Is it still possible?
// or only at #stop()? // or only at #stop()?
String c = getCasesAsString();
scriptArea.setText("" +
"//Preview \n" + c);
applyRule(call, g);
} }
private Node findRoot(Node cur) { private Node findRoot(Node cur) {
...@@ -82,6 +119,7 @@ public class InteractiveModeController { ...@@ -82,6 +119,7 @@ public class InteractiveModeController {
)); ));
gcs.setGuard(m); gcs.setGuard(m);
gcs.setBody(v); gcs.setBody(v);
c.getCases().add(gcs);
}); });
PrettyPrinter pp = new PrettyPrinter(); PrettyPrinter pp = new PrettyPrinter();
...@@ -89,6 +127,50 @@ public class InteractiveModeController { ...@@ -89,6 +127,50 @@ public class InteractiveModeController {
return pp.toString(); return pp.toString();
} }
private void applyRule(CallStatement call, Goal g) {
ObservableList<GoalNode<KeyData>> goals = model.getGoals();
GoalNode<KeyData> expandedNode;
List<GoalNode<KeyData>> collect = goals.stream().filter(keyDataGoalNode -> keyDataGoalNode.getData().getGoal().equals(g)).collect(Collectors.toList());
if (collect.isEmpty() || collect.size() > 1) {
throw new RuntimeException("Interactive Rule can not be applied, can not find goal in goal list");
} else {
expandedNode = collect.get(0);
}
RuleCommand c = new RuleCommand();
// KeyData kd = g.getData();
Map<String, String> map = new HashMap<>();
// call.getParameters().forEach((k, v) -> map.put(k.getIdentifier(), v.getData().toString()));
LOGGER.info("Execute {} with {}", call, map);
try {
KeyData kd = expandedNode.getData();
map.put("#2", call.getCommand());
EngineState estate = new EngineState(g.proof());
estate.setGoal(g);
RuleCommand.Parameters cc = c.evaluateArguments(estate, map); //reflection exception
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
c.execute(uiControl, cc, estate);
ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(g.node());
goals.remove(expandedNode);
for (Goal newGoalNode : ngoals) {
KeyData kdn = new KeyData(kd, newGoalNode.node());
goals.add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
}
} catch (Exception e) {
if (e.getClass().equals(ScriptException.class)) {
System.out.println("e.getMessage() = " + e.getMessage());
throw new ScriptCommandNotApplicableException(e, c, map);
} else {
throw new RuntimeException(e);
}
}
}
public boolean isActivated() { public boolean isActivated() {
return activated.get(); return activated.get();
} }
......
...@@ -318,7 +318,7 @@ public class TacletContextMenu extends ContextMenu { ...@@ -318,7 +318,7 @@ public class TacletContextMenu extends ContextMenu {
//System.out.println("event = [" + event + "]"); //System.out.println("event = [" + event + "]");
Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence())); Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence(), goal));
} }
/** /**
......
...@@ -40,6 +40,7 @@ public class DebuggerMainModel { ...@@ -40,6 +40,7 @@ public class DebuggerMainModel {
private ObjectProperty<InterpreterThreadState> interpreterState = new SimpleObjectProperty<>(this, "interpreterState", private ObjectProperty<InterpreterThreadState> interpreterState = new SimpleObjectProperty<>(this, "interpreterState",
InterpreterThreadState.NO_THREAD); InterpreterThreadState.NO_THREAD);
/** /**
* True, iff the execution is not possible * True, iff the execution is not possible
*/ */
......
...@@ -275,6 +275,16 @@ ...@@ -275,6 +275,16 @@
</tooltip> </tooltip>
</Button> </Button>
<Button fx:id="btnIM" onAction="#interactiveMode" disable="true">
<!--disable="${! controller.debugMode}"-->
<graphic>
<MaterialDesignIconView glyphName="HAND_POINTING_RIGHT" size="24.0"/>
</graphic>
<tooltip>
<Tooltip text="Start/Stop Interactive Mode"/>
</tooltip>
</Button>
<Pane HBox.hgrow="ALWAYS"/> <Pane HBox.hgrow="ALWAYS"/>
<Label text="Windows:"/> <Label text="Windows:"/>
<ToggleButton fx:id="togBtnCodeDock" onAction="#showCodeDock"> <ToggleButton fx:id="togBtnCodeDock" onAction="#showCodeDock">
......
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