make ModelCheckingItem editable

hhu-stups · Jul 12, 2022 · 2fb0b22 · 2fb0b22
1 parent 0ae791c
commit 2fb0b22
Show file tree

Hide file tree

Showing 7 changed files with 123 additions and 13 deletions.
diff --git a/src/main/java/de/prob2/ui/verifications/modelchecking/ModelCheckingHandleItem.java b/src/main/java/de/prob2/ui/verifications/modelchecking/ModelCheckingHandleItem.java
@@ -0,0 +1,26 @@
+package de.prob2.ui.verifications.modelchecking;
+
+
+public class ModelCheckingHandleItem {
+
+	public enum HandleType {
+		ADD, CHANGE
+	}
+
+	private HandleType handleType;
+
+	private ModelCheckingItem item;
+
+	public ModelCheckingHandleItem(HandleType handleType, ModelCheckingItem item) {
+		this.handleType = handleType;
+		this.item = item;
+	}
+
+	public HandleType getHandleType() {
+		return handleType;
+	}
+
+	public ModelCheckingItem getItem() {
+		return item;
+	}
+}
diff --git a/src/main/java/de/prob2/ui/verifications/modelchecking/ModelcheckingStage.java b/src/main/java/de/prob2/ui/verifications/modelchecking/ModelcheckingStage.java
@@ -13,6 +13,8 @@
 import de.prob2.ui.prob2fx.CurrentProject;
 import de.prob2.ui.prob2fx.CurrentTrace;
 
+import de.prob2.ui.project.machines.Machine;
+import de.prob2.ui.verifications.modelchecking.ModelCheckingHandleItem.HandleType;
 import javafx.fxml.FXML;
 import javafx.scene.control.Alert;
 import javafx.scene.control.Button;
@@ -82,6 +84,8 @@ public class ModelcheckingStage extends Stage {
 
 	private ModelCheckingItem lastItem;
 
+	private ModelCheckingHandleItem handleItem;
+
 	@Inject
 	private ModelcheckingStage(final StageManager stageManager, final ResourceBundle bundle, 
 							final CurrentTrace currentTrace, final CurrentProject currentProject, final Modelchecker modelchecker) {
@@ -171,16 +175,11 @@ private void startModelCheck() {
 			Integer tLimit = chooseTimeLimit.isSelected() ? timeLimit.getValue() : null;
 			String goal = findGoal.isSelected() ? tfFindGoal.getText() : null;
 			ModelCheckingItem modelcheckingItem = new ModelCheckingItem(id, searchStrategy, nLimit, tLimit, goal, getOptions("GOAL".equals(goal)));
-			if(currentProject.getCurrentMachine().getModelcheckingItems().stream().noneMatch(modelcheckingItem::settingsEqual)) {
-				this.hide();
-				modelchecker.checkItem(modelcheckingItem, true, false);
-				currentProject.getCurrentMachine().getModelcheckingItems().add(modelcheckingItem);
-				lastItem = modelcheckingItem;
-			} else {
-				ModelCheckingItem checkedItem = currentProject.getCurrentMachine().getModelcheckingItems().stream().filter(modelcheckingItem::settingsEqual).collect(Collectors.toList()).get(0);
-				modelchecker.checkItem(checkedItem, true, false);
-				lastItem = checkedItem;
-				this.hide();
+			if(handleItem.getHandleType() == HandleType.ADD) {
+				addItem(modelcheckingItem);
+			}
+			else {
+				changeItem(handleItem.getItem(), modelcheckingItem);
 			}
 		} else {
 			final Alert alert = stageManager.makeAlert(Alert.AlertType.ERROR, "",
@@ -190,7 +189,35 @@ private void startModelCheck() {
 			this.hide();
 		}
 	}
-
+
+	private void addItem(ModelCheckingItem modelcheckingItem) {
+		if(currentProject.getCurrentMachine().getModelcheckingItems().stream().noneMatch(modelcheckingItem::settingsEqual)) {
+			currentProject.getCurrentMachine().getModelcheckingItems().add(modelcheckingItem);
+			this.hide();
+			modelchecker.checkItem(modelcheckingItem, true, false);
+			setHandleItem(new ModelCheckingHandleItem(HandleType.CHANGE, modelcheckingItem));
+			lastItem = modelcheckingItem;
+		} else {
+			ModelCheckingItem checkedItem = currentProject.getCurrentMachine().getModelcheckingItems().stream().filter(modelcheckingItem::settingsEqual).collect(Collectors.toList()).get(0);
+			modelchecker.checkItem(checkedItem, true, false);
+			lastItem = checkedItem;
+			this.hide();
+		}
+	}
+
+	private void changeItem(ModelCheckingItem oldItem, ModelCheckingItem changedItem) {
+		Machine machine = currentProject.getCurrentMachine();
+		if(machine.getModelcheckingItems().stream().noneMatch(existing -> !oldItem.settingsEqual(existing) && changedItem.settingsEqual(existing))) {
+			machine.getModelcheckingItems().set(machine.getModelcheckingItems().indexOf(oldItem), changedItem);
+			this.hide();
+			modelchecker.checkItem(changedItem, true, false);
+			setHandleItem(new ModelCheckingHandleItem(HandleType.CHANGE, changedItem));
+			lastItem = changedItem;
+		} else {
+			this.hide();
+		}
+	}
+
 	private Set<ModelCheckingOptions.Options> getOptions(boolean goal) {
 		ModelCheckingOptions options = new ModelCheckingOptions();
 		options = options.checkDeadlocks(findDeadlocks.isSelected());
@@ -210,5 +237,43 @@ private void cancel() {
 	public ModelCheckingItem getLastItem() {
 		return lastItem;
 	}
-
+
+	public void setData(final ModelCheckingItem item) {
+		idTextField.setText(item.getId() == null ? "" : item.getId());
+
+		selectSearchStrategy.setValue(item.getSearchStrategy());
+
+		findDeadlocks.setSelected(item.getOptions().contains(ModelCheckingOptions.Options.FIND_DEADLOCKS));
+		findInvViolations.setSelected(item.getOptions().contains(ModelCheckingOptions.Options.FIND_INVARIANT_VIOLATIONS));
+		findBAViolations.setSelected(item.getOptions().contains(ModelCheckingOptions.Options.FIND_ASSERTION_VIOLATIONS));
+		stopAtFullCoverage.setSelected(item.getOptions().contains(ModelCheckingOptions.Options.STOP_AT_FULL_COVERAGE));
+
+		findOtherErrors.setSelected(!item.getOptions().contains(ModelCheckingOptions.Options.IGNORE_OTHER_ERRORS));
+
+		if (item.getNodesLimit() != null){
+			chooseNodesLimit.setSelected(true);
+			nodesLimit.getValueFactory().setValue(item.getNodesLimit());
+		} else {
+			chooseNodesLimit.setSelected(false);
+		}
+
+		if (item.getTimeLimit() != null){
+			chooseTimeLimit.setSelected(true);
+			timeLimit.getValueFactory().setValue(item.getTimeLimit());
+		} else {
+			chooseTimeLimit.setSelected(false);
+		}
+
+		if (item.getGoal() != null){
+			findGoal.setSelected(true);
+			tfFindGoal.setText(item.getGoal());
+		} else {
+			findGoal.setSelected(false);
+		}
+	}
+
+	public void setHandleItem(ModelCheckingHandleItem handleItem) {
+		this.handleItem = handleItem;
+	}
+
 }
diff --git a/src/main/java/de/prob2/ui/verifications/modelchecking/ModelcheckingView.java b/src/main/java/de/prob2/ui/verifications/modelchecking/ModelcheckingView.java
@@ -22,6 +22,9 @@
 import de.prob2.ui.verifications.IExecutableItem;
 import de.prob2.ui.verifications.ItemSelectedFactory;
 
+import de.prob2.ui.verifications.ltl.LTLHandleItem;
+import de.prob2.ui.verifications.ltl.formula.LTLFormulaItem;
+import de.prob2.ui.verifications.ltl.formula.LTLFormulaStage;
 import javafx.application.Platform;
 import javafx.beans.binding.Bindings;
 import javafx.beans.binding.BooleanExpression;
@@ -230,6 +233,9 @@ private void setContextMenus() {
 				checker.checkItem(item, true, false);
 			});
 
+			MenuItem openEditor = new MenuItem(i18n.translate("verifications.modelchecking.modelcheckingView.contextMenu.openInEditor"));
+			openEditor.setOnAction(e->showCurrentItemDialog(row.getItem()));
+
 			row.itemProperty().addListener((o, from, to) -> {
 				checkItem.disableProperty().unbind();
 				if (to != null) {
@@ -266,7 +272,7 @@ private void setContextMenus() {
 			row.contextMenuProperty().bind(
 				Bindings.when(row.emptyProperty())
 				.then((ContextMenu)null)
-				.otherwise(new ContextMenu(checkItem, searchForNewErrorsItem, removeItem)));
+				.otherwise(new ContextMenu(checkItem, searchForNewErrorsItem, removeItem, openEditor)));
 			return row;
 		});
 
@@ -294,6 +300,7 @@ private void setContextMenus() {
 	public void addModelCheck() {
 		ModelcheckingStage stageController = injector.getInstance(ModelcheckingStage.class);
 		if (!stageController.isShowing()) {
+			stageController.setHandleItem(new ModelCheckingHandleItem(ModelCheckingHandleItem.HandleType.ADD, null));
 			stageController.showAndWait();
 		}
 	}
@@ -345,4 +352,12 @@ public void selectItem(ModelCheckingItem item) {
 	public void selectJobItem(ModelCheckingJobItem item) {
 		tvChecks.getSelectionModel().select(item);
 	}
+
+	private void showCurrentItemDialog(ModelCheckingItem item) {
+		ModelcheckingStage modelcheckingStage = injector.getInstance(ModelcheckingStage.class);
+		modelcheckingStage.setData(item);
+		modelcheckingStage.setHandleItem(new ModelCheckingHandleItem(ModelCheckingHandleItem.HandleType.CHANGE, item));
+		modelcheckingStage.showAndWait();
+	}
+
 }
diff --git a/src/main/resources/de/prob2/ui/prob2.properties b/src/main/resources/de/prob2/ui/prob2.properties
@@ -858,6 +858,7 @@ verifications.modelchecking.modelcheckingStage.tooltips.timeLimit = Time Limit
 verifications.modelchecking.modelcheckingStats.elapsedTime = Time elapsed:
 verifications.modelchecking.modelcheckingStats.memoryUsage = Memory Usage:
 verifications.modelchecking.modelcheckingView.contextMenu.check = Start Model Checking
+verifications.modelchecking.modelcheckingView.contextMenu.openInEditor = Open in Editor
 verifications.modelchecking.modelcheckingView.contextMenu.remove = Remove configuration
 verifications.modelchecking.modelcheckingView.contextMenu.searchForNewErrors = Continue Model Checking
 verifications.modelchecking.modelcheckingView.contextMenu.showTrace = Show Trace

diff --git a/src/main/resources/de/prob2/ui/prob2_de.properties b/src/main/resources/de/prob2/ui/prob2_de.properties
@@ -828,6 +828,7 @@ verifications.modelchecking.modelcheckingStage.tooltips.timeLimit = Zeitlimit
 verifications.modelchecking.modelcheckingStats.elapsedTime = Verstrichene Zeit:
 verifications.modelchecking.modelcheckingStats.memoryUsage = Speicherverbrauch:
 verifications.modelchecking.modelcheckingView.contextMenu.check = Modelchecking starten
+verifications.modelchecking.modelcheckingView.contextMenu.openInEditor = In Editor \u00F6ffnen
 verifications.modelchecking.modelcheckingView.contextMenu.remove = Konfiguration entfernen
 verifications.modelchecking.modelcheckingView.contextMenu.searchForNewErrors = Modelchecking fortfahren
 verifications.modelchecking.modelcheckingView.contextMenu.showTrace = Pfad anzeigen

diff --git a/src/main/resources/de/prob2/ui/prob2_fr.properties b/src/main/resources/de/prob2/ui/prob2_fr.properties
@@ -629,6 +629,7 @@ verifications.modelchecking.modelcheckingStage.tooltips.timeLimit = Limite de te
 verifications.modelchecking.modelcheckingStats.elapsedTime = Temps ecoul\u00E9 :
 verifications.modelchecking.modelcheckingStats.memoryUsage = Utilisation de m\u00E9moire :
 verifications.modelchecking.modelcheckingView.contextMenu.check = Lancer model checking
+verifications.modelchecking.modelcheckingView.contextMenu.openInEditor = Ouvrir dans \u00E9diteur
 verifications.modelchecking.modelcheckingView.contextMenu.remove = Supprimer configration
 verifications.modelchecking.modelcheckingView.contextMenu.searchForNewErrors = Continuer model checking
 verifications.modelchecking.modelcheckingView.contextMenu.showTraceToError = Montrer l'\u00E9tat d'erreur

diff --git a/src/main/resources/de/prob2/ui/prob2_ru.properties b/src/main/resources/de/prob2/ui/prob2_ru.properties
@@ -438,6 +438,7 @@ verifications.modelchecking.modelcheckingStage.title = \u041F\u0440\u043E\u0432\
 verifications.modelchecking.modelcheckingStage.tooltips.searchStrategy = \u0421\u0442\u0440\u0430\u0442\u0435\u0433\u0438\u044F \u043F\u043E\u0438\u0441\u043A\u0430
 verifications.modelchecking.modelcheckingStats.elapsedTime = \u041F\u0440\u043E\u0448\u0435\u0434\u0448\u0435\u0435 \u0432\u0440\u0435\u043C\u044F:
 verifications.modelchecking.modelcheckingView.contextMenu.check = \u041D\u0430\u0447\u0430\u0442\u044C \u043F\u0440\u043E\u0432\u0435\u0440\u043A\u0443 \u043C\u043E\u0434\u0435\u043B\u0438
+verifications.modelchecking.modelcheckingView.contextMenu.openInEditor = \u041E\u0442\u043A\u0440\u044B\u0442\u044C \u0432 \u0440\u0435\u0434\u0430\u043A\u0442\u043E\u0440\u0435
 verifications.modelchecking.modelcheckingView.contextMenu.searchForNewErrors = \u041F\u0440\u043E\u0434\u043E\u043B\u0436\u0438\u0442\u044C \u043F\u0440\u043E\u0432\u0435\u0440\u043A\u0443 \u043C\u043E\u0434\u0435\u043B\u0438
 verifications.modelchecking.modelcheckingView.contextMenu.showTraceToError = \u041F\u043E\u043A\u0430\u0437\u0430\u0442\u044C \u0441\u043E\u0441\u0442\u043E\u044F\u043D\u0438\u0435 \u043E\u0448\u0438\u0431\u043E\u043A
 verifications.modelchecking.modelcheckingView.noModelcheckingJobs = \u0420\u0430\u0431\u043E\u0442 \u043F\u0440\u043E\u0432\u0435\u0440\u043A\u0438 \u043C\u043E\u0434\u0435\u043B\u0438 \u043D\u0435\u0442