From 4d80473332b9fd140633e6023da6b58df19a1465 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 19 Sep 2014 18:44:07 +0000
Subject: [PATCH] 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 | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java
index b3f05fc3..492ad4af 100644
--- a/prism/src/pta/DigitalClocks.java
+++ b/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()