Improve error handling in VO Manager

settings.gradle

@@ -1 +1,2 @@
 rootProject.name="prob2-ui"
+

src/main/java/de/prob2/ui/vomanager/RequirementsEditingBox.java

@@ -8,6 +8,7 @@
 import com.google.inject.Inject;
 import com.google.inject.Singleton;
 
+import de.prob.voparser.VOParseException;
 import de.prob2.ui.internal.FXMLInjected;
 import de.prob2.ui.internal.StageManager;
 import de.prob2.ui.prob2fx.CurrentProject;
@@ -89,15 +90,21 @@ public void replaceRequirement(){
 			for (ListIterator<ValidationObligation> iterator = machine.getValidationObligations().listIterator(); iterator.hasNext();) {
 				final ValidationObligation oldVo = iterator.next();
 				if (oldVo.getRequirement().equals(oldRequirement.getName())) {
-					ValidationObligation validationObligation = oldVo.changeRequirement(tfName.getText());
-					iterator.set(validationObligation);
-					requirementHandler.initListenerForVO(newRequirement, validationObligation);
+					try {
+						ValidationObligation validationObligation = new ValidationObligation(oldVo.getId(), oldVo.getExpression(), tfName.getText());
+						voChecker.parseVOExpression(validationObligation, false);
+						iterator.set(validationObligation);
+						requirementHandler.initListenerForVO(newRequirement, validationObligation);
+					} catch (VOParseException e) {
+						voChecker.handleError(this.getScene().getWindow(), e);
+					}
 				}
 			}
 		}
 	}
 
-	@FXML void historyRequirement(){
+	@FXML
+	void historyRequirement(){
 		Stage table = new RequirementHistoryTable((Requirement) voManagerStage.getSelectedRequirement());
 		stageManager.loadFXML(table, "requirement_history_box.fxml", this.getClass().getName());
 		table.show();

src/main/java/de/prob2/ui/vomanager/VOChecker.java

@@ -17,6 +17,7 @@
 import de.prob.voparser.node.Start;
 import de.prob2.ui.animation.tracereplay.ReplayTrace;
 import de.prob2.ui.animation.tracereplay.TraceChecker;
+import de.prob2.ui.internal.StageManager;
 import de.prob2.ui.prob2fx.CurrentProject;
 import de.prob2.ui.project.machines.Machine;
 import de.prob2.ui.simulation.SimulationItemHandler;
@@ -28,11 +29,15 @@
 import de.prob2.ui.verifications.modelchecking.Modelchecker;
 import de.prob2.ui.verifications.symbolicchecking.SymbolicCheckingFormulaHandler;
 import de.prob2.ui.verifications.symbolicchecking.SymbolicCheckingFormulaItem;
+import javafx.scene.control.Alert;
+import javafx.stage.Window;
 
 
 @Singleton
 public class VOChecker {
 
+	private final StageManager stageManager;
+
 	private final CurrentProject currentProject;
 
 	private final RequirementHandler requirementHandler;
@@ -50,9 +55,10 @@ public class VOChecker {
 	private final VOParser voParser;
 
 	@Inject
-	public VOChecker(final CurrentProject currentProject, final RequirementHandler requirementHandler, final Modelchecker modelchecker,
+	public VOChecker(final StageManager stageManager, final CurrentProject currentProject, final RequirementHandler requirementHandler, final Modelchecker modelchecker,
 					 final LTLFormulaChecker ltlChecker, final SymbolicCheckingFormulaHandler symbolicChecker,
 					 final TraceChecker traceChecker, final SimulationItemHandler simulationItemHandler) {
+		this.stageManager = stageManager;
 		this.voParser = new VOParser();
 		this.currentProject = currentProject;
 		this.requirementHandler = requirementHandler;
@@ -63,7 +69,7 @@ public VOChecker(final CurrentProject currentProject, final RequirementHandler r
 		this.simulationItemHandler = simulationItemHandler;
 	}
 
-	public void checkRequirement(Requirement requirement, Machine machine, VOManagerSetting setting) {
+	public void checkRequirement(Requirement requirement, Machine machine, VOManagerSetting setting) throws VOParseException{
 		if(setting == VOManagerSetting.REQUIREMENT) {
 			checkRequirementOnRequirementView(requirement);
 		} else if(setting == VOManagerSetting.MACHINE) {
@@ -72,7 +78,7 @@ public void checkRequirement(Requirement requirement, Machine machine, VOManager
 		requirementHandler.updateChecked(currentProject.get(), machine, requirement, setting);
 	}
 
-	private void checkRequirementOnRequirementView(Requirement requirement) {
+	private void checkRequirementOnRequirementView(Requirement requirement) throws VOParseException {
 		for(Machine machine : currentProject.getMachines()) {
 			for (ValidationObligation validationObligation : machine.getValidationObligations()) {
 				if(validationObligation.getRequirement().equals(requirement.getName())) {
@@ -82,7 +88,7 @@ private void checkRequirementOnRequirementView(Requirement requirement) {
 		}
 	}
 
-	private void checkRequirementOnMachineView(Requirement requirement, Machine machine) {
+	private void checkRequirementOnMachineView(Requirement requirement, Machine machine) throws VOParseException {
 		for (ValidationObligation validationObligation : machine.getValidationObligations()) {
 			if(validationObligation.getRequirement().equals(requirement.getName())) {
 				this.checkVO(validationObligation);
@@ -174,13 +180,8 @@ public void parseSequentialExpression(ASequentialVo ast, ValidationObligation VO
 	}
 
 
-	public void checkVO(ValidationObligation validationObligation) {
-		try {
-			parseVOExpression(validationObligation, true);
-		} catch (VOParseException e) {
-			e.printStackTrace();
-			// TODO
-		}
+	public void checkVO(ValidationObligation validationObligation) throws VOParseException {
+		parseVOExpression(validationObligation, true);
 	}
 
 
@@ -294,4 +295,26 @@ public void checkVT(IValidationTask validationTask) {
 		}
 	}
 
+	public void handleError(Window window, VOParseException exception) {
+		VOParseException.ErrorType errorType = exception.getErrorType();
+		String headerKey = "vomanager.error.parsing.header";
+		String contentKey;
+		switch (errorType) {
+			case PARSING:
+				contentKey = "vomanager.error.parsing.content";
+				break;
+			case SCOPING:
+				contentKey = "vomanager.error.scoping";
+				break;
+			case TYPECHECKING:
+				contentKey = "vomanager.error.typechecking";
+				break;
+			default:
+				throw new RuntimeException("VO parsing error type unknown: " + errorType);
+		}
+		final Alert alert = stageManager.makeExceptionAlert(exception, headerKey, contentKey);
+		alert.initOwner(window);
+		alert.show();
+	}
+
 }

src/main/java/de/prob2/ui/vomanager/VOEditingBox.java

@@ -198,7 +198,7 @@ private void addVO() {
 
 				requirementHandler.initListenerForVO(cbLinkRequirementChoice.getValue(), newVo);
 			} catch (VOParseException e) {
-				e.printStackTrace(); // TODO
+				voChecker.handleError(this.getScene().getWindow(), e);
 			}
 			voManagerStage.closeEditingBox();
 		} else {

src/main/java/de/prob2/ui/vomanager/VOManagerStage.java

@@ -140,13 +140,17 @@ private void initializeTables() {
 
 			MenuItem checkItem = new MenuItem(bundle.getString("common.buttons.check"));
 			checkItem.setOnAction(e -> {
-				IAbstractRequirement item = (IAbstractRequirement) row.getItem();
-				if(item instanceof Requirement) {
-					VOManagerSetting setting = cbViewSetting.getSelectionModel().getSelectedItem();
-					Machine machine = setting == VOManagerSetting.MACHINE ? (Machine) row.getTreeItem().getParent().getValue() : null;
-					voChecker.checkRequirement((Requirement) item, machine, setting);
-				} else if(item instanceof ValidationObligation) {
-					voChecker.checkVO((ValidationObligation) item);
+				try {
+					IAbstractRequirement item = (IAbstractRequirement) row.getItem();
+					if (item instanceof Requirement) {
+						VOManagerSetting setting = cbViewSetting.getSelectionModel().getSelectedItem();
+						Machine machine = setting == VOManagerSetting.MACHINE ? (Machine) row.getTreeItem().getParent().getValue() : null;
+						voChecker.checkRequirement((Requirement) item, machine, setting);
+					} else if (item instanceof ValidationObligation) {
+						voChecker.checkVO((ValidationObligation) item);
+					}
+				} catch (VOParseException exception) {
+					voChecker.handleError(this.getScene().getWindow(), exception);
 				}
 			});
 
@@ -180,12 +184,16 @@ private void initializeTables() {
 				return;
 			}
 			if (e.getClickCount() == 2 && e.getButton() == MouseButton.PRIMARY && treeItem.getChildren().isEmpty() && currentTrace.get() != null) {
-				if (nameable instanceof Requirement) {
-					VOManagerSetting setting = cbViewSetting.getSelectionModel().getSelectedItem();
-					Machine machine = setting == VOManagerSetting.MACHINE ? (Machine) treeItem.getParent().getValue() : null;
-					voChecker.checkRequirement((Requirement) nameable, machine, setting);
-				} else if (nameable instanceof ValidationObligation) {
-					voChecker.checkVO((ValidationObligation) nameable);
+				try {
+					if (nameable instanceof Requirement) {
+						VOManagerSetting setting = cbViewSetting.getSelectionModel().getSelectedItem();
+						Machine machine = setting == VOManagerSetting.MACHINE ? (Machine) treeItem.getParent().getValue() : null;
+						voChecker.checkRequirement((Requirement) nameable, machine, setting);
+					} else if (nameable instanceof ValidationObligation) {
+						voChecker.checkVO((ValidationObligation) nameable);
+					}
+				} catch (VOParseException exc) {
+					voChecker.handleError(this.getScene().getWindow(), exc);
 				}
 			}
 		});
@@ -219,8 +227,7 @@ private void updateOnMachine(Machine machine) {
 					voChecker.parseVOExpression(VO, false);
 					VO.setExpressionAst(voParser.parseFormula(VO.getExpression()).getPVo(), voChecker);
 				} catch (VOParseException e) {
-					e.printStackTrace();
-					// TODO
+					voChecker.handleError(this, e);
 				}
 			}
 		}

src/main/resources/de/prob2/ui/prob2.properties

@@ -1037,6 +1037,10 @@ vomanager.edit.vo.expression = VO Expression:
 vomanager.edit.vo.linkMachine = Link to Machine:
 vomanager.edit.vo.linkRequirement = Link to Requirement:
 vomanager.edit.vo.name = Name:
+vomanager.error.parsing.header = VO Parsing failed
+vomanager.error.parsing.content = VO Parsing failed
+vomanager.error.scoping = VO Scope Checking failed
+vomanager.error.typechecking = VO Type Checking failed
 vomanager.menu.requirements.add = Add Requirement
 vomanager.menu.vo.add = Add VO
 vomanager.table.history.column.expression = Expression

src/main/resources/de/prob2/ui/prob2_de.properties

@@ -1006,6 +1006,10 @@ vomanager.edit.vo.expression = VO Expression:
 vomanager.edit.vo.linkMachine = Link zur Maschine:
 vomanager.edit.vo.linkRequirement = Link zur Anforderung:
 vomanager.edit.vo.name = Name:
+vomanager.error.parsing.header = VO Parsing fehlgeschlagen
+vomanager.error.parsing.content = VO Parsing fehlgeschlagen
+vomanager.error.scoping = VO Scopechecking fehlgeschlagen
+vomanager.error.typechecking = VO Typchecking fehlgeschlagen
 vomanager.menu.requirements.add = Anforderung hinzuf\u00FCgen
 vomanager.menu.vo.add = VO hinzuf\u00FCgen
 vomanager.table.requirements.column.name = Name