LTLModelChecker.isSupportedLTLFormula(), for checking whether a path formula can be handled. [Joachim Klein]

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

prism/src/explicit/LTLModelChecker.java

@@ -51,8 +51,10 @@ import parser.type.TypeBool;
 import parser.type.TypePathBool;
 import prism.DA;
 import prism.LTL2RabinLibrary;
+import prism.ModelType;
 import prism.PrismComponent;
 import prism.PrismException;
+import prism.PrismLangException;
 import prism.PrismFileLog;
 import prism.PrismLog;
 
@@ -111,6 +113,30 @@ public class LTLModelChecker extends PrismComponent
 	{
 		return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl, constantValues);
 	}
+	
+	
+	/**
+	 * Returns {@code true} if expression {@code expr} is a formula that can be handled by
+	 * LTLModelChecker for the given ModelType.
+	 */
+	public static boolean isSupportedLTLFormula(ModelType modelType, Expression expr) throws PrismLangException
+	{
+		if (!expr.isPathFormula(true)) {
+			return false;
+		}
+		if (Expression.containsTemporalTimeBounds(expr)) {
+			if (modelType.continuousTime()) {
+				// Only support temporal bounds for discrete time models
+				return false;
+			}
+			
+			if (!expr.isSimplePathFormula()) {
+				// Only support temporal bounds for simple path formulas
+				return false;
+			}
+		}
+		return true;
+	}
 
 	/**
 	 * Extract maximal state formula from an LTL path formula, model check them (with passed in model checker) and

prism/src/prism/LTLModelChecker.java

@@ -61,6 +61,29 @@ public class LTLModelChecker extends PrismComponent
 		super(parent);
 	}
 
+	/**
+	 * Returns {@code true} if expression {@code expr} is a formula that can be handled by
+	 * LTLModelChecker for the given ModelType.
+	 */
+	public static boolean isSupportedLTLFormula(ModelType modelType, Expression expr) throws PrismLangException
+	{
+		if (!expr.isPathFormula(true)) {
+			return false;
+		}
+		if (Expression.containsTemporalTimeBounds(expr)) {
+			if (modelType.continuousTime()) {
+				// Only support temporal bounds for discrete time models
+				return false;
+			}
+			
+			if (!expr.isSimplePathFormula()) {
+				// Only support temporal bounds for simple path formulas
+				return false;
+			}
+		}
+		return true;
+	}
+
 	/**
 	 * Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression,
 	 * in which atomic propositions are represented by ExpressionLabel objects.