From 8b7990d6abc2e0af99639e671047a3d4eaf1bf0e Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 1 Nov 2010 20:36:16 +0000
Subject: [PATCH] Better checks for convexity in (A-R) PTA model checking
 (again).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2214 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/pta/Modules2PTA.java | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/prism/src/pta/Modules2PTA.java b/prism/src/pta/Modules2PTA.java
index 504843d6..a9ed6cec 100644
--- a/prism/src/pta/Modules2PTA.java
+++ b/prism/src/pta/Modules2PTA.java
@@ -188,8 +188,15 @@ public class Modules2PTA
 				pcValues.setValue(pc, i);
 				// Evaluate (partially) invariant for this PC value
 				invar = (Expression) invar.evaluatePartially(null, pcValues).simplify();
-				// Add invariant to transition (unless "true")
+				// The (partial) invariant should now be a conjunction of clock constraints (or true)
+				// Split into parts, convert to constraints and add to PTA (unless "true")
+				// If expression is not (syntactically) convex, complain
 				exprs = ParserUtils.splitConjunction(invar);
+				for (Expression ex : exprs) {
+					if (!(Expression.isTrue(ex) || Expression.isFalse(ex))) {
+						checkIsSimpleClockConstraint(ex);
+					}
+				}
 				for (Expression ex : exprs) {
 					if (!Expression.isTrue(ex)) {
 						for (Constraint c : exprToConstraint(ex, pta)) {