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); } }