LTL2DA: Improve error handling.

In some cases, errors in LTL2RabinLibrary should be treated as
errors (when the formula contains temporal bounds), other times
we want to give jltl2dstar / the external LTL2DA tools another
try.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10287 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/automata/LTL2DA.java

@@ -103,8 +103,16 @@ public class LTL2DA extends PrismComponent
 					getLog().println("Taking deterministic Rabin automaton from library...");
 				}
 			} catch (Exception e) {
-				getLog().println("Warning: Exception during attempt to construct DRA using the LTL2RabinLibrary:");
-				getLog().println(" "+e.getMessage());
+				if (containsTemporalBounds) {
+					// there is (currently) no other way to translate LTL with temporal bounds,
+					// so treat an exception as a "real" one
+					throw e;
+				} else {
+					// there is the possibility that we might be able to construct
+					// an automaton below, just issue a warning
+					getLog().println("Warning: Exception during attempt to construct DRA using the LTL2RabinLibrary:");
+					getLog().println(" "+e.getMessage());
+				}
 			}
 		}