From 1fdd5e9bf9313afc1edc3a29ac69f9ce94c1516b Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 21 Apr 2008 14:39:15 +0000
Subject: [PATCH] LTL properties can't have time bounds.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@765 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/NondetModelChecker.java | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index 13c88537..f3096f37 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -32,9 +32,11 @@ import java.util.*;
 import jdd.*;
 import dv.*;
 import mtbdd.*;
+import simulator.SimulatorException;
 import sparse.*;
 import hybrid.*;
 import parser.ast.*;
+import parser.visitor.ASTTraverse;
 import jltl2dstar.*;
 
 /*
@@ -392,6 +394,22 @@ public class NondetModelChecker extends StateModelChecker
 			throw new PrismException("Fairness is not supported for LTL properties");
 		}
 		
+		// Can't do LTL with time-bounded variants of the temporal operators
+		try {
+			expr.accept(new ASTTraverse()
+			{
+				public void visitPre(ExpressionTemporal e) throws PrismLangException
+				{
+					if (e.getLowerBound() != null) throw new PrismLangException(e.getOperatorSymbol());
+					if (e.getUpperBound() != null) throw new PrismLangException(e.getOperatorSymbol());
+				}
+			});
+		} catch (PrismLangException e) {
+			String s = "Temporal operators (like "+e.getMessage()+")";
+			s += " cannot have time bounds for LTL properties";
+			throw new PrismException(s);
+		}
+		
 		// For LTL model checking routines 
 		mcLtl = new LTLModelChecker(prism, this);