imported patch time-bounded-not-supported-message.patch

prism/src/prism/LTLModelChecker.java

@@ -324,7 +324,7 @@ public class LTLModelChecker extends PrismComponent
 
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
-				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
+				throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
 			if (!expr.isSimplePathFormula()) {

prism/src/prism/NondetModelChecker.java

@@ -1555,7 +1555,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
 				JDD.Deref(statesOfInterest);
-				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
+				throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
 			if (expr.isSimplePathFormula()) {
@@ -1569,18 +1569,18 @@ public class NondetModelChecker extends NonProbModelChecker
 				expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
 			} else {
 				JDD.Deref(statesOfInterest);
-				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+				throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
 			}
 		}
 
 		// Can't do "dfa" properties yet
 		if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) {
 			JDD.Deref(statesOfInterest);
-			throw new PrismException("Model checking for \"dfa\" specifications not supported yet");
+			throw new PrismNotSupportedException("Model checking for \"dfa\" specifications not supported yet");
 		}
 
 		if (Expression.containsTemporalRewardBounds(expr)) {
-			throw new PrismException("Can not handle reward bounds via deterministic automata.");
+			throw new PrismNotSupportedException("Can not handle reward bounds via deterministic automata.");
 		}
 
 		if (Expression.isHOA(expr)) {

prism/src/prism/ProbModelChecker.java

@@ -1015,25 +1015,25 @@ public class ProbModelChecker extends NonProbModelChecker
 
 		if (Expression.containsTemporalRewardBounds(expr)) {
 			JDD.Deref(statesOfInterest);
-			throw new PrismException("Can not handle reward bounds via deterministic automata.");
+			throw new PrismNotSupportedException("Can not handle reward bounds via deterministic automata.");
 		}
 
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
 				JDD.Deref(statesOfInterest);
-				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
+				throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
 			if (!expr.isSimplePathFormula()) {
 				JDD.Deref(statesOfInterest);
-				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+				throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
 			}
 		}
 
 		// Can't do "dfa" properties yet
 		if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) {
 			JDD.Deref(statesOfInterest);
-			throw new PrismException("Model checking for \"dfa\" specifications not supported yet");
+			throw new PrismNotSupportedException("Model checking for \"dfa\" specifications not supported yet");
 		}
 
 		if (Expression.isHOA(expr)) {