From 0559014a2fc1de7f6656e7449c818556e7b69ef4 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 4 Oct 2018 17:32:06 +0200 Subject: [PATCH] GUISimulator: harden against exceptions (1) In general, for user actions (a_...), ensure that setComputing(false) is called even if the underlying computing resulted in an exception. This ensures that the buttons/menu items of the simulator are properly enabled again and we don't get into a deadlock situation where we can't even start a new path. (2) For the automatic step actions, ensure that the path display is updated even if there is an exception, as there may have been intermediate steps that had succeeded before the error occurred. --- .../userinterface/simulator/GUISimulator.java | 86 +++++++++++++------ 1 file changed, 59 insertions(+), 27 deletions(-) diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 2c55d43f..1ce269b6 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -520,10 +520,20 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect setComputing(true); - if (isOldUpdate()) { - engine.computeTransitionsForCurrentState(); + try { + if (isOldUpdate()) { + engine.computeTransitionsForCurrentState(); + } + engine.automaticTransitions(noSteps, displayPathLoops); + } catch (PrismException e) { + this.error(e.getMessage()); + guiMultiModel.getHandler().modelParseFailed(e, false); + guiMultiModel.tabToFront(); + + // Even if there was an exception, we continue and try + // to update the path display, as there may be intermediate steps + // that have succeeded } - engine.automaticTransitions(noSteps, displayPathLoops); // Update model/path/tables/lists pathTableModel.updatePathTable(); @@ -534,12 +544,12 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // Update display repaintLists(); updatePathInfo(); - setComputing(false); - } catch (PrismException e) { this.error(e.getMessage()); - guiMultiModel.getHandler().modelParseFailed((PrismLangException) e, false); + guiMultiModel.getHandler().modelParseFailed(e, false); guiMultiModel.tabToFront(); + } finally { + setComputing(false); } } @@ -556,10 +566,22 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } setComputing(true); - if (isOldUpdate()) { - engine.computeTransitionsForCurrentState(); + + try { + if (isOldUpdate()) { + engine.computeTransitionsForCurrentState(); + } + engine.automaticTransitions(time, displayPathLoops); + } catch (PrismException e) { + this.error(e.getMessage()); + guiMultiModel.getHandler().modelParseFailed(e, false); + guiMultiModel.tabToFront(); + + // Even if there was an exception, we continue and try + // to update the path display, as there may be intermediate steps + // that have succeeded } - engine.automaticTransitions(time, displayPathLoops); + // Update model/path/tables/lists pathTableModel.updatePathTable(); int height = (int) pathTable.getPreferredSize().getHeight(); @@ -569,11 +591,13 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // Update display repaintLists(); updatePathInfo(); - setComputing(false); } catch (PrismException e) { this.error(e.getMessage()); } + finally { + setComputing(false); + } } /** Backtrack to a certain time. */ @@ -588,9 +612,10 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // Update display repaintLists(); updatePathInfo(); - setComputing(false); } catch (PrismException e) { this.error(e.getMessage()); + } finally { + setComputing(false); } } @@ -606,9 +631,10 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // Update display repaintLists(); updatePathInfo(); - setComputing(false); } catch (PrismException e) { this.error(e.getMessage()); + } finally { + setComputing(false); } } @@ -624,24 +650,28 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // Update display repaintLists(); updatePathInfo(); - setComputing(false); } catch (PrismException e) { this.error(e.getMessage()); + } finally { + setComputing(false); } } /** Remove the prefix of the current path up to the given path step. */ public void a_removePreceding(int step) throws PrismException { - setComputing(true); - engine.removePrecedingStates(step); - // Update model/path/tables/lists - pathTableModel.updatePathTable(); - updateTableModel.updateUpdatesTable(); - // Update display - repaintLists(); - updatePathInfo(); - setComputing(false); + try { + setComputing(true); + engine.removePrecedingStates(step); + // Update model/path/tables/lists + pathTableModel.updatePathTable(); + updateTableModel.updateUpdatesTable(); + // Update display + repaintLists(); + updatePathInfo(); + } finally { + setComputing(false); + } } public void a_manualUpdate() @@ -681,13 +711,12 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // Update display repaintLists(); updatePathInfo(); - setComputing(false); } catch (NumberFormatException e) { this.error("The Auto update \'no. steps\' parameter is invalid.\nIt must be a positive integer representing a step in the path table"); - setComputing(false); } catch (PrismException e) { this.error(e.getMessage()); + } finally { setComputing(false); } } @@ -736,9 +765,10 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect return; setComputing(true); engine.exportPath(getChooserFile()); - setComputing(false); } catch (PrismException e) { error(e.getMessage()); + } finally { + setComputing(false); } } @@ -750,9 +780,10 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect Graph graphModel = new Graph(); guiProp.getGraphHandler().addGraph(graphModel); engine.plotPath(graphModel); - setComputing(false); } catch (PrismException e) { error(e.getMessage()); + } finally { + setComputing(false); } } @@ -817,7 +848,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect getPrism().getMainLog().resetNumberOfWarnings(); parser.State initialStateObject = initialState == null ? null : new parser.State(initialState, parsedModel); new SimPathPlotThread(this, engine, parsedModel, initialStateObject, simPathDetails, maxPathLength, graphModel).start(); - setComputing(false); // store initial state for next time lastInitialState = initialState; @@ -828,6 +858,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect guiMultiModel.getHandler().modelParseFailed((PrismLangException) e, false); guiMultiModel.tabToFront(); } + } finally { + setComputing(false); } }