Add error message if attempting to check an LTL formula on a PTA (with digital clocks).

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

prism/src/pta/DigitalClocks.java

@@ -318,6 +318,22 @@ public class DigitalClocks
 	{
 		ASTElement ast;
 
+		// LTL not handled (look in any P operators)
+		try {
+			propertyToCheck.accept(new ASTTraverse()
+			{
+				public void visitPost(ExpressionProb e) throws PrismLangException
+				{
+					if (!e.getExpression().isSimplePathFormula()) {
+						throw new PrismLangException("The digital clocks method does not support LTL properties");
+					}
+				}
+			});
+		} catch (PrismLangException e) {
+			e.setASTElement(propertyToCheck);
+			throw e;
+		}
+		
 		// Bounded properties not yet handled.
 		try {
 			propertyToCheck.accept(new ASTTraverse()