From 43ffa810db907e07b2988f4acc97e757dd867e20 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sun, 24 Jul 2016 17:27:08 +0000
Subject: [PATCH] Catch invalid negative time bounds in PTA model checking.

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

diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java
index 507ed4fc..c89a68d4 100644
--- a/prism/src/pta/PTAModelChecker.java
+++ b/prism/src/pta/PTAModelChecker.java
@@ -215,6 +215,10 @@ public class PTAModelChecker extends PrismComponent
 			// Get time bound info (is always of form <=T or <T)
 			timeBound = exprTemp.getUpperBound().evaluateInt(constantValues);
 			timeBoundStrict = exprTemp.upperBoundIsStrict();
+			// Check for non-allowed time bounds (negative)
+			if (timeBound < (timeBoundStrict ? 1 : 0)) {
+				throw new PrismLangException("Negative bound in " + exprTemp);
+			}
 			// Modify PTA to include time bound; get new target
 			targetLocs = buildTimeBoundIntoPta(pta, targetLocs, timeBound, timeBoundStrict);
 			mainLog.println("New PTA: " + pta.infoString());