From c8d545b4f2dc82a82277a28d9d024c0b9aca46a3 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 14 Sep 2016 11:34:22 +0000
Subject: [PATCH] ast.RelOp: for negate, optionally keep the strictness of the
 operator [with Steffen Maercker and Marcus Daum]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11817 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/ast/RelOp.java | 39 +++++++++++++++++++++++----------
 1 file changed, 27 insertions(+), 12 deletions(-)

diff --git a/prism/src/parser/ast/RelOp.java b/prism/src/parser/ast/RelOp.java
index a4eb9843..dd6c5bcb 100644
--- a/prism/src/parser/ast/RelOp.java
+++ b/prism/src/parser/ast/RelOp.java
@@ -21,9 +21,9 @@ public enum RelOp
 		}
 
 		@Override
-		public RelOp negate() throws PrismLangException
+		public RelOp negate(boolean keepStrictness) throws PrismLangException
 		{
-			return LEQ;
+			return (keepStrictness ? LT : LEQ);
 		}
 	},
 	GEQ(">=") {
@@ -34,9 +34,9 @@ public enum RelOp
 		}
 
 		@Override
-		public RelOp negate() throws PrismLangException
+		public RelOp negate(boolean keepStrictness) throws PrismLangException
 		{
-			return LT;
+			return (keepStrictness ? LEQ : LT);
 		}
 	},
 	MIN("min=") {
@@ -47,7 +47,7 @@ public enum RelOp
 		}
 
 		@Override
-		public RelOp negate() throws PrismLangException
+		public RelOp negate(boolean keepStrictness) throws PrismLangException
 		{
 			return MAX;
 		}
@@ -66,9 +66,9 @@ public enum RelOp
 		}
 
 		@Override
-		public RelOp negate() throws PrismLangException
+		public RelOp negate(boolean keepStrictness) throws PrismLangException
 		{
-			return GEQ;
+			return (keepStrictness ? GT : GEQ);
 		}
 	},
 	LEQ("<=") {
@@ -79,9 +79,9 @@ public enum RelOp
 		}
 
 		@Override
-		public RelOp negate() throws PrismLangException
+		public RelOp negate(boolean keepStrictness) throws PrismLangException
 		{
-			return GT;
+			return (keepStrictness ? GEQ : GT);
 		}
 	},
 	MAX("max=") {
@@ -92,14 +92,14 @@ public enum RelOp
 		}
 
 		@Override
-		public RelOp negate() throws PrismLangException
+		public RelOp negate(boolean keepStrictness) throws PrismLangException
 		{
 			return MIN;
 		}
 	},
 	EQ("=") {
 		@Override
-		public RelOp negate() throws PrismLangException
+		public RelOp negate(boolean keepStrictness) throws PrismLangException
 		{
 			throw new PrismLangException("Cannot negate " + this);
 		}
@@ -162,8 +162,23 @@ public enum RelOp
 
 	/**
 	 * Returns the negated form of this operator.
+	 * <br>
+	 * Equivalent to {@code negate(false)}.
 	 */
-	public abstract RelOp negate() throws PrismLangException;
+	public RelOp negate() throws PrismLangException
+	{
+		return negate(false);
+	}
+
+	/**
+	 * Returns the negated form of this operator.
+	 * Depending on the flag {@code keepStrictness},
+	 * the strictness is preserved. E.g., with
+	 * {@code keepStrictness == true} the operator "&lt;"
+	 * is turned into "&gt;", with {@code keepStrictness == false}
+	 * the operator "&lt;" is turned into "&gt=;"
+	 */
+	public abstract RelOp negate(boolean keepStrictness) throws PrismLangException;
 
 	/**
 	 * Returns the RelOp object corresponding to a (string) symbol,