From a702c7ca648049ed7aac582e20b87cd993af9e4b Mon Sep 17 00:00:00 2001
From: Ernst Moritz Hahn <emhahn@cs.ox.ac.uk>
Date: Fri, 17 May 2013 00:07:31 +0000
Subject: [PATCH] fix for operator comparism which did not work in certain
 cases

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

diff --git a/prism/src/param/BoxRegion.java b/prism/src/param/BoxRegion.java
index 228c415e..56157278 100644
--- a/prism/src/param/BoxRegion.java
+++ b/prism/src/param/BoxRegion.java
@@ -298,14 +298,19 @@ final class BoxRegion extends Region {
 			StateValues newValues = new StateValues(op1.getNumStates(), factory.getInitialState());
 			boolean allDecided = true;
 			for (int state = 0; state < op1.getNumStates(); state++) {
-				Function op1Val = op1.getStateValueAsFunction(state);
-				Function op2Val = op2.getStateValueAsFunction(state);
+				StateValue op1Val = op1.getStateValue(state);
+				StateValue op2Val = op2.getStateValue(state);
+				Function op1ValFn = op1Val instanceof Function ? (Function) op1Val : null;
+				Function op2ValFn = op2Val instanceof Function ? (Function) op2Val : null;
 				if (op == Region.EQ) {
-					if (op1Val.equals(op2Val)) {
+					if (op1Val instanceof StateBoolean) {
+						newValues.setStateValue(state, op1Val.equals(op2Val));						
+					}
+					else if (op1Val.equals(op2Val)) {
 						newValues.setStateValue(state, true);			
-					} else if (checker.check(region, op1Val.subtract(op2Val), true)) {
+					} else if (checker.check(region, op1ValFn.subtract(op2ValFn), true)) {
 						newValues.setStateValue(state, false);	
-					} else if (checker.check(region, op2Val.subtract(op1Val), true)) {
+					} else if (checker.check(region, op2ValFn.subtract(op1ValFn), true)) {
 						newValues.setStateValue(state, false);	
 					} else {
 						allDecided = false;
@@ -313,16 +318,16 @@ final class BoxRegion extends Region {
 					}
 				} else {
 					boolean strict = op == Region.GT || op == Region.LT;
-					Function cmpTrue = (op == Region.LT || op == Region.LE) ? op2Val.subtract(op1Val) : op1Val.subtract(op2Val);
+					Function cmpTrue = (op == Region.LT || op == Region.LE) ? op2ValFn.subtract(op1ValFn) : op1ValFn.subtract(op2ValFn);
 					if (checker.check(region, cmpTrue, strict)) {
 						newValues.setStateValue(state, true);
 					} else {
-						Function cmpFalse = (op == Region.LT || op == Region.LE) ? op1Val.subtract(op2Val) : op2Val.subtract(op1Val);
+						Function cmpFalse = (op == Region.LT || op == Region.LE) ? op1ValFn.subtract(op2ValFn) : op2ValFn.subtract(op1ValFn);
 						if (checker.check(region, cmpFalse, !strict)) {
 							newValues.setStateValue(state, false);	
 						} else {
 							allDecided = false;
-							lastFunction = op2Val.subtract(op1Val);
+							lastFunction = op2ValFn.subtract(op1ValFn);
 							break;
 						}
 					}