diff --git a/doc b/doc deleted file mode 160000 index 294f2fe61188314a0e50fe80ce2de2070df85599..0000000000000000000000000000000000000000 --- a/doc +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 294f2fe61188314a0e50fe80ce2de2070df85599 diff --git a/keydeps/README.user b/keydeps/README.user index d16784df3e7dd2d3363e839be2252b772e1376c3..51782b1672d1c6f75b7130c56e40ce662d4a6a3c 100755 --- a/keydeps/README.user +++ b/keydeps/README.user @@ -33,3 +33,7 @@ mvn install:install-file -Dfile=$COMPONENTS/../libs/recoderKey.jar\ -DartifactId=recoder \ -Dversion=2.7\ -Dpackaging=jar \ + + +//insgesamt efach in der Kommandozeile das eingeben + diff --git a/keydeps/lib/components/key.core.jar b/keydeps/lib/components/key.core.jar index f5ce60b1539379e01fe81758b667f44446a3864d..33aefead34f8d0f6301a1b52f0e564130e9a51d2 100644 Binary files a/keydeps/lib/components/key.core.jar and b/keydeps/lib/components/key.core.jar differ diff --git a/keydeps/lib/components/key.ui.jar b/keydeps/lib/components/key.ui.jar index bae07dc3dd49f31a9cd1d46dc7bddcb54774dc93..e17f3e8813791ce5cb85df97cc3f3e47c4224866 100644 Binary files a/keydeps/lib/components/key.ui.jar and b/keydeps/lib/components/key.ui.jar differ diff --git a/keydeps/lib/components/key.util.jar b/keydeps/lib/components/key.util.jar index f6f9a47aaf9f921c5066abff60639b544242eea9..e2869cf3796335a510fec82ec7d2c4621c57f68c 100644 Binary files a/keydeps/lib/components/key.util.jar and b/keydeps/lib/components/key.util.jar differ diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java index 54270547e5c4386daedf18aa8bab9830d354eb6d..b579909f77c6108ac2592755b95631713682eb28 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java @@ -1,12 +1,12 @@ package edu.kit.iti.formal.psdbg.interpreter; import de.uka.ilkd.key.api.KeYApi; -import de.uka.ilkd.key.api.ProjectedNode; import de.uka.ilkd.key.api.ProofApi; import de.uka.ilkd.key.api.ScriptApi; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; +import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import edu.kit.iti.formal.psdbg.interpreter.assignhook.InterpreterOptionsHook; import edu.kit.iti.formal.psdbg.interpreter.assignhook.KeyAssignmentHook; @@ -19,14 +19,15 @@ import edu.kit.iti.formal.psdbg.parser.Visitor; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; import lombok.Getter; +import org.key_project.util.collection.ImmutableList; import java.io.File; import java.io.IOException; -import java.security.Key; import java.util.Arrays; import java.util.Collection; import java.util.List; import java.util.Set; +import java.util.stream.Collectors; /** * @author Alexander Weigl @@ -202,11 +203,13 @@ public class InterpreterBuilder { if (proof == null || keyEnvironment == null) throw new IllegalStateException("Call proof(..) before startState"); - final ProofApi pa = new ProofApi(proof, keyEnvironment); - final ProjectedNode root = pa.getFirstOpenGoal(); - final KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof()); - final GoalNode startGoal = new GoalNode<>(null, keyData, keyData.isClosedNode()); - return startState(startGoal); + ImmutableList openGoals = proof.getSubtreeGoals(proof.root()); + List> goals = openGoals.stream().map(g -> + new GoalNode<>(null, new KeyData(g, keyEnvironment, proof), false)) + .collect(Collectors.toList()); + interpreter.newState(goals); + return this; + } private InterpreterBuilder startState(GoalNode startGoal) { diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java index 266b46ec5682cb0caff2ee2918fd0396c4686711..d7051d0dc3fbad30744682fd36b5ffabd916438d 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java @@ -37,6 +37,7 @@ public class InspectionView extends BorderPane { ); public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu(); + public SequentOptionsMenu sequentOptionsMenu = new SequentOptionsMenu(model.get()); @FXML @Getter private ComboBox> frames; @@ -160,6 +161,11 @@ public class InspectionView extends BorderPane { goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY()); } + public void showSequentOptions(MouseEvent actionEvent) { + Node n = (Node) actionEvent.getTarget(); + sequentOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY()); + } + public InspectionModel getModel() { return model.get(); } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java new file mode 100644 index 0000000000000000000000000000000000000000..b55fe2727f25433f82cc67cf5cd7d529dc024662 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java @@ -0,0 +1,225 @@ +package edu.kit.iti.formal.psdbg.gui.controls; + +import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.pp.*; +import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; +import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; +import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade; +import edu.kit.iti.formal.psdbg.termmatcher.Matchings; +import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath; +import javafx.beans.Observable; +import javafx.beans.property.*; +import javafx.collections.FXCollections; +import javafx.collections.ObservableList; +import javafx.fxml.FXML; +import javafx.scene.Node; +import javafx.scene.control.Label; +import javafx.scene.control.ListCell; +import javafx.scene.control.ListView; +import javafx.scene.control.TextArea; +import javafx.scene.input.MouseEvent; +import javafx.scene.layout.BorderPane; +import javafx.scene.layout.Pane; + +import java.util.Collections; +import java.util.HashMap; +import java.util.Map; + +public class SequentMatcher extends BorderPane { + + + public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu(); + + @FXML + private SequentView sequentView; + + @FXML + private ListView> goalView; + + @FXML + private TextArea matchpattern; + + @FXML + private ListView> matchingsView; + + @FXML + private Label nomatchings; //only shown when no matchings found, else always hidden + + private Map cursorPosition = new HashMap<>(); + + public SequentMatcher() { + Utils.createWithFXML(this); + + + selectedGoalNodeToShow.addListener((observable, oldValue, newValue) -> { + sequentView.setGoal(newValue.getData().getGoal()); + sequentView.setNode(newValue.getData().getNode()); + calculateLookupTable(); + + } + ); + + goalView.getSelectionModel().selectedItemProperty().addListener((prop, old, nnew) -> + selectedGoalNodeToShow.setValue(nnew) + ); + + goalView.setCellFactory(GoalNodeListCell::new); + + + goals.addListener((observable, oldValue, newValue) -> goalView.setItems(newValue)); + + matchingsView.getSelectionModel().selectedItemProperty().addListener((observable, oldValue, newValue) -> { + if (newValue != null) { + newValue.forEach((name, mp) -> { + PosInOccurrence pio = mp.pio(); + Range r = cursorPosition.get(pio); + sequentView.setStyleClass(r.start(),r.end(), "sequent-highlight"); + + System.out.println("Highlight " + r.start() + " " + r.end()); + }); + + } + }); + } + + private void calculateLookupTable() { + sequentView.update(null); + cursorPosition.clear(); + LogicPrinter.PosTableStringBackend backend = sequentView.getBackend(); + SequentPrintFilter filter = new IdentitySequentPrintFilter(); + filter.setSequent(selectedGoalNodeToShow.get().getData().getNode().sequent()); + for (int i = 0; i < sequentView.getText().length(); i++) { + try { + Range range = backend.getPositionTable().rangeForIndex(i, sequentView.getLength()); + PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(i, filter); + if (pis != null && pis.getPosInOccurrence() != null) { + Term term = pis.getPosInOccurrence().subTerm(); + cursorPosition.put(pis.getPosInOccurrence(), range); + } + } catch (NullPointerException e) { + e.printStackTrace(); + } + } + } + + public void showGoalOptions(MouseEvent actionEvent) { + Node n = (Node) actionEvent.getTarget(); + goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY()); + } + + public void startMatch() { + Matchings matchings = MatcherFacade.matches(matchpattern.getText(), getSelectedGoalNodeToShow().getData().getNode().sequent(), true); + ObservableList> resultlist = FXCollections.observableArrayList(matchings); + + //If no matchings found, add "No matchings found" + if (resultlist.isEmpty()) { + matchingsView.setVisible(false); + nomatchings.setVisible(true); + } else { + nomatchings.setVisible(false); + matchingsView.setItems(resultlist); + matchingsView.setVisible(true); + } + + + + + } + + //alle aktuellen nicht geschlossene Ziele -> alle leaves später (open+closed) + private final ListProperty> goals = new SimpleListProperty<>(this, "goals", FXCollections.observableArrayList()); + + private final ListProperty> matchingresults = new SimpleListProperty<>(this, "matchingresults", FXCollections.observableArrayList()); + + public ObservableList> getMatchingresults() { + return matchingresults.get(); + } + + + public ObservableList> getResults() { + return results.get(); + } + + public ListProperty> resultsProperty() { + return results; + } + + public void setResults(ObservableList> results) { + this.results.set(results); + } + + private final ListProperty> results = new SimpleListProperty<>(this, "results", FXCollections.observableArrayList()); + + + //sicht user selected + private final ObjectProperty> selectedGoalNodeToShow = new SimpleObjectProperty<>(this, "selectedGoalNodeToShow"); + + public ObservableList> getGoals() { + return goals.get(); + } + + public ListProperty> goalsProperty() { + return goals; + } + + public void setGoals(ObservableList> goals) { + this.goals.set(goals); + } + + public GoalNode getSelectedGoalNodeToShow() { + return selectedGoalNodeToShow.get(); + } + + public ObjectProperty> selectedGoalNodeToShowProperty() { + return selectedGoalNodeToShow; + } + + + + public void setSelectedGoalNodeToShow(GoalNode selectedGoalNodeToShow) { + this.selectedGoalNodeToShow.set(selectedGoalNodeToShow); + } + + + public ListView> getMatchingsView() { + return matchingsView; + } + + public void setMatchingsView(ListView> matchingsView) { + this.matchingsView = matchingsView; + } + + public ListProperty> matchingresultsProperty() { + return matchingresults; + } + + public void setMatchingresults(ObservableList> matchingresults) { + this.matchingresults.set(matchingresults); + } + + /** + * Cells for GoalView + */ + private class GoalNodeListCell extends ListCell> { + + public GoalNodeListCell(ListView> goalNodeListView) { + itemProperty().addListener(this::update); + goalOptionsMenu.selectedViewOptionProperty().addListener(this::update); + } + + private void update(Observable observable) { + if (getItem() == null) { + setText(""); + return; + } + KeyData item = getItem().getData(); + String text = "n/a"; + if (goalOptionsMenu.getSelectedViewOption() != null) { + text = goalOptionsMenu.getSelectedViewOption().getText(item); + } + //setStyle("-fx-font-size: 12pt;"); + setText(text); + } + } +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java new file mode 100644 index 0000000000000000000000000000000000000000..1a23f8f9b82335e1e4389c51fbc95a44d9f3fd56 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java @@ -0,0 +1,69 @@ +package edu.kit.iti.formal.psdbg.gui.controls; + +import com.google.common.collect.BiMap; +import com.google.common.collect.HashBiMap; +import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger; +import edu.kit.iti.formal.psdbg.gui.model.InspectionModel; +import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; +import javafx.beans.property.ObjectProperty; +import javafx.beans.property.SimpleObjectProperty; +import javafx.event.ActionEvent; +import javafx.event.EventHandler; +import javafx.fxml.FXML; +import javafx.fxml.FXMLLoader; +import javafx.scene.Parent; +import javafx.scene.Scene; +import javafx.scene.control.*; +import javafx.stage.Modality; +import javafx.stage.Stage; +import javafx.stage.StageStyle; +import org.dockfx.DockNode; + +import java.util.function.Function; + +public class SequentOptionsMenu extends ContextMenu { + + + private final InspectionModel model; + @FXML + private MenuItem openSequentMatcher; + + + public SequentOptionsMenu(InspectionModel model) { + Utils.createWithFXML(this); + this.model = model; + openSequentMatcher.setOnAction(new EventHandler() { + @Override + public void handle(ActionEvent event) { + + + try { + SequentMatcher root1 = new SequentMatcher(); + root1.setGoals(model.getGoals()); + root1.setSelectedGoalNodeToShow(model.getSelectedGoalNodeToShow()); + root1.getStyleClass().add("sequent-view"); + + Stage stage = new Stage(); + stage.setTitle("Sequent Matcher"); + Scene scene = new Scene(root1); + scene.getStylesheets().addAll( + // ProofScriptDebugger.class.getClass().getResource("debugger-ui.css").toExternalForm() + getClass().getResource("/edu/kit/iti/formal/psdbg/gui/debugger-ui.css") + .toExternalForm()); + + stage.setScene(scene); + + stage.show(); + + + } catch (Exception e) { + e.printStackTrace(); + System.out.println(e); + } + } + }); + + } + + +} \ No newline at end of file diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java index 15ac28931e654839e830c6e14dcd9a5180354000..754767b6ac0b0a4f037206bab86441401be27ef1 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java @@ -66,6 +66,7 @@ public class SequentView extends CodeArea { int insertionPoint = hit.getInsertionIndex(); try { PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter); + if (pis != null) { Range r = backend.getPositionTable().rangeForIndex(insertionPoint, getLength()); hightlightRange(r.start(), r.end()); @@ -134,6 +135,7 @@ public class SequentView extends CodeArea { filter = new IdentitySequentPrintFilter(); filter.setSequent(sequent); + ProgramPrinter prgPrinter = new ProgramPrinter(new StringWriter()); this.backend = new LogicPrinter.PosTableStringBackend(80); @@ -208,7 +210,7 @@ public class SequentView extends CodeArea { Matchings m = MatcherFacade.matches(pattern, node.get().sequent(), true); if (m.size() == 0) return false; Map va = m.first(); - System.out.println(va);//TODO remove + //System.out.println(va);//TODO remove for (MatchPath mp : va.values()) { System.out.println(mp.pio()); highlightTerm(mp.pio()); @@ -226,4 +228,8 @@ public class SequentView extends CodeArea { Range r = backend.getInitialPositionTable().rangeForPath(path); setStyle(r.start(), r.end(), Collections.singleton("search-highlight")); } + + public LogicPrinter.PosTableStringBackend getBackend() { + return backend; + } } diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.fxml b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.fxml index 9e870a64db19a1f990f85f6c965e6ef60605887a..a1d47845e84c4a5a7ce3eae472b50c1c9fa75d93 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.fxml +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.fxml @@ -34,7 +34,7 @@ - + +
+ + + +
+
+ + +
+ +
+
+ + +