Browse Source

GUI computation threads: Catch more errors (e.g. CuddOutOfMemoryException) and use the new error(Exception) handling

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10483 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 11 years ago
parent
commit
68e0a80b98
  1. 5
      prism/src/userinterface/GUIPrism.java
  2. 4
      prism/src/userinterface/model/computation/BuildModelThread.java
  3. 4
      prism/src/userinterface/model/computation/ComputeSteadyStateThread.java
  4. 4
      prism/src/userinterface/model/computation/ComputeTransientThread.java
  5. 4
      prism/src/userinterface/model/computation/ExportBuiltModelThread.java
  6. 16
      prism/src/userinterface/properties/GUIExperiment.java
  7. 2
      prism/src/userinterface/properties/computation/ExportResultsThread.java
  8. 4
      prism/src/userinterface/properties/computation/ModelCheckThread.java
  9. 4
      prism/src/userinterface/properties/computation/SimulateModelCheckThread.java

5
prism/src/userinterface/GUIPrism.java

@ -97,6 +97,11 @@ public class GUIPrism extends JFrame
System.err.println("Error: "+e.getMessage());
System.exit(1);
}
catch(jdd.JDD.CuddOutOfMemoryException e)
{
System.err.println("Error: "+e.getMessage());
System.exit(1);
}
}
/**

4
prism/src/userinterface/model/computation/BuildModelThread.java

@ -65,8 +65,8 @@ public class BuildModelThread extends GUIComputationThread
// Do build
try {
prism.buildModel();
} catch (PrismException e) {
error(e.getMessage());
} catch (Exception e) {
error(e);
SwingUtilities.invokeLater(new Runnable()
{
public void run()

4
prism/src/userinterface/model/computation/ComputeSteadyStateThread.java

@ -76,8 +76,8 @@ public class ComputeSteadyStateThread extends GUIComputationThread
// Do Computation
try {
prism.doSteadyState(exportType, exportFile, null);
} catch (PrismException e) {
error(e.getMessage());
} catch (Exception e) {
error(e);
SwingUtilities.invokeLater(new Runnable()
{
public void run()

4
prism/src/userinterface/model/computation/ComputeTransientThread.java

@ -78,8 +78,8 @@ public class ComputeTransientThread extends GUIComputationThread
// Do Computation
try {
prism.doTransient(transientTime, exportType, exportFile, null);
} catch (PrismException e) {
error(e.getMessage());
} catch (Exception e) {
error(e);
SwingUtilities.invokeLater(new Runnable()
{
public void run()

4
prism/src/userinterface/model/computation/ExportBuiltModelThread.java

@ -112,8 +112,8 @@ public class ExportBuiltModelThread extends GUIComputationThread
}
});
return;
} catch (PrismException e2) {
error(e2.getMessage());
} catch (Exception e2) {
error(e2);
SwingUtilities.invokeAndWait(new Runnable()
{
public void run()

16
prism/src/userinterface/properties/GUIExperiment.java

@ -230,9 +230,9 @@ public class GUIExperiment
try {
definedMFConstants = undefinedConstants.getMFConstantValues();
prism.setPRISMModelConstants(definedMFConstants);
} catch (PrismException e) {
} catch (Exception e) {
// in case of error, report it (in log only), store as result, and go on to the next model
errorLog(e.getMessage());
errorLog(e);
setMultipleErrors(definedMFConstants, null, e);
undefinedConstants.iterateModel();
continue;
@ -244,9 +244,9 @@ public class GUIExperiment
info = null;
info = GUISimulationPicker.defineSimulationWithDialog(guiProp.getGUI(), propertyToCheck.getExpression(), prism.getPRISMModel(), "("
+ definedMFConstants + ")");
} catch (PrismException e) {
} catch (Exception e) {
// in case of error, report it (in log only), store as result, and go on to the next model
errorLog(e.getMessage());
errorLog(e);
setMultipleErrors(definedMFConstants, null, e);
undefinedConstants.iterateModel();
continue;
@ -284,9 +284,9 @@ public class GUIExperiment
// update progress meter
// (all properties simulated simultaneously so can't get more accurate feedback at the moment anyway)
table.progressChanged();
} catch (PrismException e) {
} catch (Exception e) {
// in case of error, report it (in log only), store as result, and go on to the next model
errorLog(e.getMessage());
errorLog(e);
setMultipleErrors(definedMFConstants, null, e);
undefinedConstants.iterateModel();
continue;
@ -322,9 +322,9 @@ public class GUIExperiment
res = prism.modelCheckSimulator(propertiesFile, propertyToCheck.getExpression(), definedPFConstants, initialState,
info.getMaxPathLength(), info.createSimulationMethod());
}
} catch (PrismException e) {
} catch (Exception e) {
// in case of error, report it (in log only), store exception as the result and proceed
errorLog(e.getMessage());
errorLog(e);
res = new Result(e);
}
// store result of model checking

2
prism/src/userinterface/properties/computation/ExportResultsThread.java

@ -106,7 +106,7 @@ public class ExportResultsThread extends Thread
out.flush();
out.close();
}
catch (IOException e) {
catch (Exception e) {
SwingUtilities.invokeLater(new Runnable()
{
public void run()

4
prism/src/userinterface/properties/computation/ModelCheckThread.java

@ -104,9 +104,9 @@ public class ModelCheckThread extends GUIComputationThread
// Do model checking
try {
result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(i));
} catch (PrismException e) {
} catch (Exception e) {
result = new Result(e);
error(e.getMessage());
error(e);
}
ic.interrupt();
try {

4
prism/src/userinterface/properties/computation/SimulateModelCheckThread.java

@ -117,10 +117,10 @@ public class SimulateModelCheckThread extends GUIComputationThread
// do simulation
results = prism.modelCheckSimulatorSimultaneously(pf, properties, definedPFConstants, initialState, maxPathLength, method);
method.reset();
} catch (PrismException e) {
} catch (Exception e) {
// in the case of an error which affects all props, store/report it
resultError = e;
error(e.getMessage());
error(e);
}
//after collecting the results stop all of the clock icons
for (int i = 0; i < clkThreads.size(); i++) {

Loading…
Cancel
Save