s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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.
master
Joachim Klein 8 years ago
parent
737ad9cd22
commit
0559014a2f
1 changed files with 59 additions and 27 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 86
      prism/src/userinterface/simulator/GUISimulator.java

86
prism/src/userinterface/simulator/GUISimulator.java
View File

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

Write Preview
Loading…
Cancel
Save