From 750923dfbf3e5acfa4c337827b6a037f0c12a4e2 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 16 Feb 2017 13:21:38 +0000
Subject: [PATCH] (param/exact) fix handling of != in parametric/exact engine
 (with Linda Leuschner)

Missing case for NE operator in BoxRegion.cmpOp. This affects the check routines
for the != operator in the parametric/exact engines, e.g., for state formulas
such as s!=t


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

diff --git a/prism/src/param/BoxRegion.java b/prism/src/param/BoxRegion.java
index 56157278..84890049 100644
--- a/prism/src/param/BoxRegion.java
+++ b/prism/src/param/BoxRegion.java
@@ -316,6 +316,19 @@ final class BoxRegion extends Region {
 						allDecided = false;
 						break;
 					}
+				} else if (op == Region.NE) {
+					if (op1Val instanceof StateBoolean) {
+						newValues.setStateValue(state, !op1Val.equals(op2Val));
+					} else if (op1Val.equals(op2Val)) {
+						newValues.setStateValue(state, false);
+					} else if (checker.check(region, op1ValFn.subtract(op2ValFn), true)) {
+						newValues.setStateValue(state, true);
+					} else if (checker.check(region, op2ValFn.subtract(op1ValFn), true)) {
+						newValues.setStateValue(state, true);
+					} else {
+						allDecided = false;
+						break;
+					}
 				} else {
 					boolean strict = op == Region.GT || op == Region.LT;
 					Function cmpTrue = (op == Region.LT || op == Region.LE) ? op2ValFn.subtract(op1ValFn) : op1ValFn.subtract(op2ValFn);