GUI: Handle StackOverflowErrors gracefully

prism/src/userinterface/GUIComputationThread.java

@@ -26,6 +26,7 @@
 
 package userinterface;
 
+import common.StackTraceHelper;
 import prism.*;
 
 /**
@@ -35,7 +36,10 @@ public class GUIComputationThread extends Thread
 {
 	protected GUIPlugin plug;
 	protected Prism prism;
-	
+
+	/** Limit on number of lines for logging a stack trace */
+	protected int STACK_TRACE_LIMIT = StackTraceHelper.DEFAULT_STACK_TRACE_LIMIT;
+
 	/** Creates a new instance of GUIComputationThread */
 	public GUIComputationThread(GUIPlugin plug)
 	{
@@ -50,16 +54,33 @@ public class GUIComputationThread extends Thread
 		errorDialog(s);
 	}
 
-	/** Report an error for an Exception (in log and popup dialog) */
-	public void error(Exception e)
-	{
+	/**
+	 * Report an error for an Exception/Error/Throwable (in log and popup dialog).
+	 * <br>
+	 * In case of a serious error that is unlikely to be recovered from
+	 * (i.e., an Error that is not a StackOverflowError), rethrow the error.
+	 */
+	public void error(Throwable e) {
 		if (e instanceof jdd.JDD.CuddOutOfMemoryException) {
 			error(e.getMessage()+".\nTry increasing the value of \"CUDD max. memory\" in the options and then restart PRISM");
 		} else if (e instanceof PrismException) {
 			error(e.getMessage());
+		} else if (e instanceof StackOverflowError) {
+			String hint = "\nTry increasing the value of the Java stack size (via the -javastack argument)";
+
+			// use message with stack trace for log
+			errorLog(e.toString() + "\n" + StackTraceHelper.asString(e, STACK_TRACE_LIMIT) + hint);
+
+			// use short message, without stack trace, for dialog
+			errorDialog(e.toString() + hint);
 		} else {
 			error(e.toString()+"\nThis is an unexpected error, it might be a good idea to restart PRISM");
 		}
+
+		// for a serious error, i.e., derived from Error, except stack overflow, rethrow the error
+		if (e instanceof Error && !(e instanceof StackOverflowError)) {
+			throw (Error)e;
+		}
 	}
 
 	/** Report an error (in log) */
@@ -68,8 +89,8 @@ public class GUIComputationThread extends Thread
 		logln("\nError: " + s + ".");
 	}
 
-	/** Report an Exception error (in log) */
-	public void errorLog(Exception e)
+	/** Report an Exception/Throwable error (in log) */
+	public void errorLog(Throwable e)
 	{
 		if (e instanceof PrismException || e instanceof jdd.JDD.CuddOutOfMemoryException) {
 			logln("\nError: " + e.getMessage() + ".");

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

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

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

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

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

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

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

@@ -112,7 +112,7 @@ public class ExportBuiltModelThread extends GUIComputationThread
 					}
 				});
 				return;
-			} catch (Exception e2) {
+			} catch (Throwable e2) {
 				error(e2);
 				SwingUtilities.invokeAndWait(new Runnable()
 				{

prism/src/userinterface/properties/GUIExperiment.java

@@ -35,6 +35,9 @@ import prism.*;
 import userinterface.*;
 
 import javax.swing.*;
+
+import common.StackTraceHelper;
+
 import java.util.*;
 import userinterface.util.*;
 
@@ -241,6 +244,13 @@ public class GUIExperiment
 						setMultipleErrors(definedMFConstants, null, e);
 						undefinedConstants.iterateModel();
 						continue;
+					} catch (StackOverflowError e) {
+						// in case of stack overflow, report it (in log only),
+						// store as PrismException in result, and go on to the next model
+						errorLog(e.toString() + "\n" + StackTraceHelper.asString(e, STACK_TRACE_LIMIT));
+						setMultipleErrors(definedMFConstants, null, new PrismException("Stack overflow"));
+						undefinedConstants.iterateModel();
+						continue;
 					}
 
 					// collect information for simulation if required
@@ -295,6 +305,13 @@ public class GUIExperiment
 							setMultipleErrors(definedMFConstants, null, e);
 							undefinedConstants.iterateModel();
 							continue;
+						} catch (StackOverflowError e) {
+							// in case of stack overflow, report it (in log only),
+							// store as PrismException in result, and go on to the next model
+							errorLog(e.toString() + "\n" + StackTraceHelper.asString(e, STACK_TRACE_LIMIT));
+							setMultipleErrors(definedMFConstants, null, new PrismException("Stack overflow"));
+							undefinedConstants.iterateModel();
+							continue;
 						}
 					} else {
 						// iterate through as many properties as necessary
@@ -331,6 +348,11 @@ public class GUIExperiment
 								// in case of error, report it (in log only), store exception as the result and proceed
 								errorLog(e);
 								res = new Result(e);
+							} catch (StackOverflowError e) {
+								// in case of stack overflow, report it (in log only),
+								// store as PrismException in result, and proceed
+								errorLog(e.toString() + "\n" + StackTraceHelper.asString(e, STACK_TRACE_LIMIT));
+								res = new Result(new PrismException("Stack overflow"));
 							}
 							// store result of model checking
 							SwingUtilities.invokeAndWait(new Runnable()

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

@@ -107,6 +107,11 @@ public class ModelCheckThread extends GUIComputationThread
 			} catch (Exception e) {
 				result = new Result(e);
 				error(e);
+			} catch (StackOverflowError e) {
+				// convert the StackOverflowError to a PrismException, as the result handling
+				// expects Exception instead of Error objects
+				result = new Result(new PrismException("Stack overflow"));
+				error(e);
 			}
 			ic.interrupt();
 			try {

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

@@ -121,6 +121,11 @@ public class SimulateModelCheckThread extends GUIComputationThread
 				// in the case of an error which affects all props, store/report it
 				resultError = e;
 				error(e);
+			} catch (StackOverflowError e) {
+				// in the case of an error which affects all props, store/report it
+				// convert to a PrismException for result
+				resultError = new PrismException("Stack overflow");
+				error(e);
 			}
 			//after collecting the results stop all of the clock icons
 			for (int i = 0; i < clkThreads.size(); i++) {
@@ -164,9 +169,13 @@ public class SimulateModelCheckThread extends GUIComputationThread
 					// do simulation
 					result = prism.modelCheckSimulator(pf, pf.getProperty(i), definedPFConstants, initialState, maxPathLength, method);
 					method.reset();
-				} catch (PrismException e) {
+				} catch (Exception e) {
 					result = new Result(e);
-					error(e.getMessage());
+					error(e);
+				} catch (StackOverflowError e) {
+					// store as PrismException in result
+					result = new Result(new PrismException("Stack overflow"));
+					error(e);
 				}
 				ict.interrupt();
 				while (!ict.canContinue) {