Browse Source

PrismCL: Catch unhandled Exceptions instead of delegating to default Java handling

We are now catching unhandled Exceptions and errorAndExit. Previously,
we relied on the Java handling, which would print the stack trace and kill
the main thread.

However, it seems that in the presence of thread pools (e.g., with the JAS
library used by param/exact model checking), an unhandled exception would kill
the main thread but not terminate PRISM. This could be triggered
e.g. with

prism prism-examples/dice/dice.pm -pf 'P>0.5[ F s=7 ]' -exact

which generates an unhandled ClassCastException and previously would make
PRISM hang indefinitely.



git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11537 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
commit
0632eb656a
  1. 11
      prism/src/prism/PrismCL.java

11
prism/src/prism/PrismCL.java

@ -29,6 +29,8 @@ package prism;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.PrintWriter;
import java.io.StringWriter;
import java.net.UnknownHostException;
import java.util.ArrayList;
import java.util.List;
@ -211,6 +213,15 @@ public class PrismCL implements PrismModelListener
mainLog.println(st);
}
errorAndExit(e.getMessage() + ".\nTip: Try using the -cuddmaxmem switch to increase the memory available to CUDD");
} catch (Exception e) {
// We catch Exceptions here ourself to ensure that we actually exit
// In the presence of thread pools (e.g., in the JAS library when using -exact),
// the main thread dying does not necessarily quit the program...
StringWriter sw = new StringWriter();
sw.append("\n");
e.printStackTrace(new PrintWriter(sw));
mainLog.print(sw.toString());
errorAndExit("Caught unhandled exception, aborting...");
}
}

Loading…
Cancel
Save