Commit 6b02ec1c authored by Lulu Luong's avatar Lulu Luong

Cyclicbarrier + userinteraction UI

Contextmenu for watches
varass sync
parent c8b796af
Pipeline #40785 passed with stages
in 3 minutes and 3 seconds
......@@ -5,6 +5,7 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException;
......@@ -20,6 +21,7 @@ import de.uka.ilkd.key.rule.IfFormulaInstantiation;
import de.uka.ilkd.key.rule.Rule;
import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.TacletApp;
import de.uka.ilkd.key.rule.inst.InstantiationEntry;
import de.uka.ilkd.key.rule.inst.SVInstantiations;
import edu.kit.iti.formal.psdbg.RuleCommandHelper;
import edu.kit.iti.formal.psdbg.ValueInjector;
......@@ -53,11 +55,16 @@ import lombok.RequiredArgsConstructor;
import lombok.Setter;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.DefaultImmutableMap;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableMap;
import org.key_project.util.collection.ImmutableMapEntry;
import java.io.IOException;
import java.math.BigInteger;
import java.util.*;
import java.util.concurrent.BrokenBarrierException;
import java.util.concurrent.CyclicBarrier;
/**
* @author Alexander Weigl
......@@ -75,6 +82,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
private Scanner scanner = new Scanner(System.in);
@Getter
@Setter
private TacletAppSelectionDialogService tacletAppSelectionDialogService;
......@@ -138,7 +146,6 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
if (!rules.containsKey(call.getCommand())) {
throw new IllegalStateException();
}
//FIXME duplicate of ProofScriptCommandBuilder
RuleCommand c = new RuleCommand();
State<KeyData> state = interpreter.getCurrentState();
GoalNode<KeyData> expandedNode = state.getSelectedGoalNode();
......@@ -168,27 +175,48 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
if (e instanceof ScriptException.IndistinctFormula) {
List<TacletApp> matchingapps = ((ScriptException.IndistinctFormula) e).getMatchingApps();
List<TacletApp> completed_matchingapps = new ArrayList<>();
for (TacletApp tacletApp : matchingapps) {
try {
TacletInstantiationModel tim = new TacletInstantiationModel(tacletApp, kd.getGoal().sequent(), kd.getGoal().getLocalNamespaces(), null, kd.getGoal());
TacletApp newTA = tim.createTacletApp();
completed_matchingapps.add(newTA);
} catch (SVInstantiationException svie) {
// Not buildable tacletapps
}
}
ObservableList<String> obsMatchApps = FXCollections.observableArrayList();
int linenr = call.getStartPosition().getLineNumber();
matchingapps.forEach(k -> obsMatchApps.add(tacletAppIntoString(k, kd.getGoal(), linenr)));
//TODO: open window here
completed_matchingapps.forEach(k -> obsMatchApps.add(tacletAppIntoString(k, kd.getGoal(), linenr)));
//open window here
CyclicBarrier cyclicBarrier = new CyclicBarrier(2, tacletAppSelectionDialogService.getRunnable());
IndistinctWindow indistinctWindow = new IndistinctWindow(obsMatchApps);
tacletAppSelectionDialogService.setCyclicBarrier(cyclicBarrier);
tacletAppSelectionDialogService.setPane(indistinctWindow);
tacletAppSelectionDialogService.showDialog();
TacletApp chosenApp = matchingapps.get(tacletAppSelectionDialogService.getUserIndexInput());
TacletInstantiationModel tim = new TacletInstantiationModel(chosenApp, kd.getGoal().sequent(), kd.getGoal().getLocalNamespaces(), null, kd.getGoal());
try {
TacletApp newTA = tim.createTacletApp();
newTA.execute(kd.getGoal(), kd.getProof().getServices());
cyclicBarrier.await();
} catch (InterruptedException ex) {
exceptionsolved = true;
} catch (SVInstantiationException svie) {
} catch (BrokenBarrierException ex) {
}
}
TacletApp chosenApp = completed_matchingapps.get(tacletAppSelectionDialogService.getUserIndexInput());
System.out.println("chosenapp = " + tacletAppIntoString(chosenApp, kd.getGoal(), linenr));
chosenApp.execute(kd.getGoal(), kd.getProof().getServices());
exceptionsolved = true;
}
if (!exceptionsolved) {
if (interpreter.isStrictMode()) {
......@@ -250,18 +278,27 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
int occ = rch.getOccurence(tacletApp);
tacletAppString = String.format("%s formula=' %s ' on=' %s ' occ=%d;",
tacletAppString = String.format("%s formula='%s' on='%s' occ=%d ",
tapName,
sfTerm.trim(),
onTerm.trim(),
occ);
// add missing instantiations
if (!tacletApp.ifInstsComplete()) {
SVInstantiations sv = tacletApp.instantiations();
//TODO:
String ifInstString = "";
if (tacletApp.ifInstsComplete()) {
Iterator<ImmutableMapEntry<SchemaVariable, InstantiationEntry<?>>> iterator = tacletApp.instantiations().pairIterator();
while (iterator.hasNext()) {
ImmutableMapEntry<SchemaVariable, InstantiationEntry<?>> mapentry = iterator.next();
ifInstString += String.format("inst_%s ='%s' ", mapentry.key().name(), mapentry.value().getInstantiation());
//"inst_" + mapentry.key().name() + "=" + mapentry.value().getInstantiation();
}
}
tacletAppString += ifInstString;
tacletAppString += "; ";
tacletAppString += String.format("(linenumber = %d)", linenumber);
return tacletAppString;
......
......@@ -3,19 +3,22 @@ package edu.kit.iti.formal.psdbg.interpreter;
import javafx.collections.ObservableList;
import javafx.event.EventHandler;
import javafx.fxml.FXMLLoader;
import javafx.geometry.Orientation;
import javafx.scene.control.Button;
import javafx.scene.control.ListView;
import javafx.scene.control.ScrollPane;
import javafx.scene.control.TextField;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.BorderPane;
import javafx.scene.layout.FlowPane;
import javafx.scene.layout.HBox;
import javafx.scene.layout.VBox;
import javafx.scene.text.Text;
import lombok.Getter;
import java.util.List;
public class IndistinctWindow extends BorderPane {
public class IndistinctWindow extends VBox {
@Getter
int indexOfSelected = -1;
......@@ -24,11 +27,16 @@ public class IndistinctWindow extends BorderPane {
public IndistinctWindow(ObservableList<String> matchApps) {
//Top
ScrollPane scrollPane = new ScrollPane();
this.setPrefWidth(700);
//Center
ListView<String> listView = new ListView<String>(matchApps);
scrollPane.setContent(listView);
this.setTop(scrollPane);
this.getChildren().add(listView);
//Bottom
accept = new Button();
accept.setText("Accept");
this.getChildren().add(accept);
listView.setOnMouseClicked(new EventHandler<MouseEvent>() {
@Override
......@@ -38,19 +46,6 @@ public class IndistinctWindow extends BorderPane {
}
});
//Center
/*
HBox hbox = new HBox();
Text inputlabel = new Text("Enter a number:");
TextField textField = new TextField();
hbox.getChildren().addAll(inputlabel, textField);
this.setCenter(hbox);
*/
//Bottom
accept = new Button();
accept.setText("Accept");
this.setBottom(accept);
}
}
......@@ -16,9 +16,7 @@ import lombok.Getter;
import lombok.Setter;
import java.util.List;
import java.util.concurrent.Callable;
import java.util.concurrent.CountDownLatch;
import java.util.concurrent.FutureTask;
import java.util.concurrent.*;
public abstract class TacletAppSelectionDialogService {
......@@ -28,10 +26,18 @@ public abstract class TacletAppSelectionDialogService {
@Getter
int userIndexInput;
private CountDownLatch latch = new CountDownLatch(1);
private Runnable runnable;
@Setter
private CyclicBarrier cyclicBarrier;
public void showDialog() {
Platform.runLater(new Runnable() {
runnable = getRunnable();
Platform.runLater(runnable);
}
public Runnable getRunnable() {
return new Runnable() {
@Override
public void run() {
Stage stage = new Stage();
......@@ -45,14 +51,21 @@ public abstract class TacletAppSelectionDialogService {
public void handle(MouseEvent event) {
getIndex();
if (userIndexInput != -1) {
stage.close();
try {
stage.close();
cyclicBarrier.await();
} catch (InterruptedException ex) {
} catch (BrokenBarrierException ex) {
}
}
}
});
stage.showAndWait();
latch.countDown();
}
});
};
}
......
......@@ -64,11 +64,10 @@ public class GoalOptionsMenu extends ContextMenu {
Utils.showInfoDialog("Select a goal", "Select a goal", "Please select a goal first.");
return;
}
VariableAssignment var_assignm = model.getSelectedGoalNodeToShow().getAssignments();
//VariableAssignment var_assignm = model.getSelectedGoalNodeToShow().getAssignments();
Stage stage = new Stage();
stage.setTitle("Variable Assignment");
VariableAssignmentWindow vaw = new VariableAssignmentWindow(var_assignm);
VariableAssignmentWindow vaw = new VariableAssignmentWindow(model);
Scene scene = new Scene(vaw);
stage.setScene(scene);
......
package edu.kit.iti.formal.psdbg.gui.controls;
import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import edu.kit.iti.formal.psdbg.interpreter.Evaluator;
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.VariableNotDefinedException;
import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.StringLiteral;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.event.ActionEvent;
import javafx.event.EventHandler;
import javafx.fxml.FXML;
import javafx.scene.control.*;
import javafx.scene.control.cell.PropertyValueFactory;
import javafx.scene.layout.BorderPane;
import lombok.Getter;
import javax.script.ScriptEngine;
import javax.script.ScriptEngineManager;
import java.util.*;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
......@@ -28,11 +31,19 @@ public class VariableAssignmentWindow extends BorderPane {
TableView special_tableView;
@FXML
TableView history_tableView;
TableView watches_tableView;
@FXML
TextArea match_variables;
@FXML
TabPane tabPane;
@FXML
Tab watchesTab;
private ContextMenu contextMenu;
private VariableAssignment assignment;
/** Non special Variables that don't start with __ **/
......@@ -41,30 +52,27 @@ public class VariableAssignmentWindow extends BorderPane {
/** Variables that start with __ **/
private ObservableList<VariableModel> specialModel;
private ObservableList<VariableModel> historyModel = FXCollections.observableArrayList();
private ObservableList<VariableModel> watchesModel = FXCollections.observableArrayList();
private String matchexp;
private ScriptEngineManager mgr = new ScriptEngineManager();
private ScriptEngine engine = mgr.getEngineByName("JavaScript");
private List<VariableModel> matchlist_declarative = new ArrayList<>();
private List<VariableModel> matchlist_special = new ArrayList<>();
private Evaluator evaluator;
public VariableAssignmentWindow(VariableAssignment assignment) {
private InspectionModel inspectionModel;
public VariableAssignmentWindow(InspectionModel inspectionModel) {
//TODO: reduce size of constructor
Utils.createWithFXML(this);
if (assignment != null) {
fillInVariableModelsLists(assignment);
}
this.inspectionModel = inspectionModel;
declarative_tableView.setEditable(false);
special_tableView.setEditable(false);
history_tableView.setEditable(false);
watches_tableView.setEditable(false);
//Table Colums for declarative_tableView
TableColumn decl_varCol = new TableColumn("Variable");
......@@ -86,7 +94,6 @@ public class VariableAssignmentWindow extends BorderPane {
new PropertyValueFactory<VariableModel,String>("varval")
);
declarative_tableView.setItems(declarativeModel);
declarative_tableView.getColumns().addAll(decl_varCol, decl_typeCol, decl_valCol);
//Table Colums for special_tableView
......@@ -109,19 +116,18 @@ public class VariableAssignmentWindow extends BorderPane {
new PropertyValueFactory<VariableModel,String>("varval")
);
special_tableView.setItems(specialModel);
special_tableView.getColumns().addAll(spec_varCol, spec_typeCol, spec_valCol);
//Table Colums for history_tableView
//Table Colums for watches_tableView
TableColumn hist_varCol = new TableColumn("Variable");
TableColumn hist_typeCol = new TableColumn("Type");
TableColumn hist_valCol = new TableColumn("Value");
//Set Colums width proportional to windows with
hist_varCol.prefWidthProperty().bind(history_tableView.widthProperty().divide(3));
hist_typeCol.prefWidthProperty().bind(history_tableView.widthProperty().divide(3));
hist_valCol.prefWidthProperty().bind(history_tableView.widthProperty().divide(3));
hist_varCol.prefWidthProperty().bind(watches_tableView.widthProperty().divide(3));
hist_typeCol.prefWidthProperty().bind(watches_tableView.widthProperty().divide(3));
hist_valCol.prefWidthProperty().bind(watches_tableView.widthProperty().divide(3));
hist_varCol.setCellValueFactory(
new PropertyValueFactory<VariableModel, String>("varname")
......@@ -133,8 +139,8 @@ public class VariableAssignmentWindow extends BorderPane {
new PropertyValueFactory<VariableModel, String>("varval")
);
history_tableView.setItems(historyModel);
history_tableView.getColumns().addAll(hist_varCol, hist_typeCol, hist_valCol);
watches_tableView.setItems(watchesModel);
watches_tableView.getColumns().addAll(hist_varCol, hist_typeCol, hist_valCol);
//Row factory added
declarative_tableView.setRowFactory(tv -> new TableRow<VariableModel>() {
......@@ -159,7 +165,17 @@ public class VariableAssignmentWindow extends BorderPane {
}
});
evaluator = new Evaluator(assignment, null);
inspectionModel.currentInterpreterGoalProperty().addListener(new ChangeListener<GoalNode<KeyData>>() {
@Override
public void changed(ObservableValue<? extends GoalNode<KeyData>> observable, GoalNode<KeyData> oldValue, GoalNode<KeyData> newValue) {
refresh();
}
});
watches_tableView.setOnContextMenuRequested(evt -> {
getContextMenu().show(this, evt.getScreenX(), evt.getScreenY());
});
refresh();
}
/**
......@@ -215,6 +231,9 @@ public class VariableAssignmentWindow extends BorderPane {
}
/**
* Evaluates String in Textfield matchexp as Expression and puts it into the Tab tabWatches
*/
@FXML
private void evaluate() {
matchexp = match_variables.getText();
......@@ -227,8 +246,12 @@ public class VariableAssignmentWindow extends BorderPane {
value.getType().toString(),
value.getData().toString());
historyModel.add(vm);
history_tableView.refresh();
watchesModel.add(vm);
watches_tableView.refresh();
//focus on tab
SingleSelectionModel<Tab> selectionModel = tabPane.getSelectionModel();
selectionModel.select(watchesTab);
} catch (Exception e) {
System.out.println("No evaluable expression");
......@@ -257,29 +280,6 @@ public class VariableAssignmentWindow extends BorderPane {
special_tableView.refresh();
}
/**
* Extracts variable from given string, though only 1 variable is possibla
*
* @param expression string to extract variable
* @return variable starting with ? only if there's only 1 match, else ""
*/
private String getVariable(String expression) {
Pattern pattern = Pattern.compile("\\?\\w+");
Matcher matcher = pattern.matcher(expression);
List<String> variables_matches = new ArrayList<>();
while (matcher.find()) {
if (!variables_matches.contains(matcher.group())) {
variables_matches.add(matcher.group());
}
}
//if there are multiple variables return null
if (variables_matches.size() != 1) {
return "";
}
return variables_matches.get(0);
}
/**
* Calculate matching results of matchexpression with given list
......@@ -302,6 +302,42 @@ public class VariableAssignmentWindow extends BorderPane {
return matchlist;
}
public ContextMenu getContextMenu() {
if (contextMenu == null) {
contextMenu = new ContextMenu();
MenuItem deleteWatch = new MenuItem("Delete Watch");
deleteWatch.setOnAction(new EventHandler<ActionEvent>() {
@Override
public void handle(ActionEvent event) {
try {
int selected = watches_tableView.getSelectionModel().getFocusedIndex();
if (0 <= selected && selected < watchesModel.size()) {
watchesModel.remove(selected);
watches_tableView.refresh();
}
} catch (Exception e) {
}
}
});
contextMenu.getItems().add(deleteWatch);
}
return contextMenu;
}
private void refresh() {
assignment = inspectionModel.getCurrentInterpreterGoal().getAssignments();
evaluator = new Evaluator(assignment, null);
if (assignment != null) {
fillInVariableModelsLists(assignment);
}
declarative_tableView.setItems(declarativeModel);
special_tableView.setItems(specialModel);
declarative_tableView.refresh();
special_tableView.refresh();
}
public static class VariableModel {
@Getter
......@@ -317,4 +353,5 @@ public class VariableAssignmentWindow extends BorderPane {
this.varval = varval;
}
}
}
......@@ -199,8 +199,6 @@
</graphic>
</CheckMenuItem>
<CheckMenuItem fx:id="miUserInter" onAction="#showUserInteractionW"
text="Show Userinteraction Window"/>
<CheckMenuItem fx:id="miCommandHelp" onAction="#showCommandHelp"
accelerator="F1"
text="Show Command Help">
......
......@@ -31,7 +31,7 @@
</BorderPane>
</top>
<center>
<TabPane tabClosingPolicy="UNAVAILABLE">
<TabPane fx:id="tabPane" tabClosingPolicy="UNAVAILABLE">
<tabs>
<Tab text="Script Variables">
<TableView fx:id="declarative_tableView"></TableView>
......@@ -39,8 +39,8 @@
<Tab text="KeY Control Variables">
<TableView fx:id="special_tableView"></TableView>
</Tab>
<Tab text="History">
<TableView fx:id="history_tableView"></TableView>
<Tab fx:id="watchesTab" text="Watches">
<TableView fx:id="watches_tableView"></TableView>
</Tab>
</tabs>
</TabPane>
......
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