From 2cedf62ad9fb7c11e463b965c88a6c397246f283 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 15 Jan 2021 16:11:47 +0000
Subject: [PATCH] Array sup-norm methods in PrismUtils consistently check only
 over common elements.

Assertions that checked that, e.g., arrays were the same size have been removed.
(These are disabled in the JDK by default anyway)

Some value iteration methods, which take in an "init" array of known values
can violate these assertions, e.g., when it is created to be over size for efficiency
in an abstraction refinement loop.
---
 prism/src/prism/PrismUtils.java | 19 ++++---------------
 1 file changed, 4 insertions(+), 15 deletions(-)

diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java
index 0efc89e5..1afde7cd 100644
--- a/prism/src/prism/PrismUtils.java
+++ b/prism/src/prism/PrismUtils.java
@@ -177,9 +177,6 @@ public class PrismUtils
 	 */
 	public static <X> boolean doublesAreClose(HashMap<X,Double> map1, HashMap<X,Double> map2, double epsilon, boolean abs)
 	{
-		if (map1.size() != map2.size()) {
-			return false;
-		}
 		Set<Entry<X,Double>> entries = map1.entrySet();
 		for (Entry<X,Double> entry : entries) {
 			double d1 = (double) entry.getValue();
@@ -193,7 +190,7 @@ public class PrismUtils
 						return false;
 				}
 			} else {
-				return false;
+				// Only check over common elements
 			}
 		}
 		return true;
@@ -205,7 +202,6 @@ public class PrismUtils
 	 */
 	public static <X> double measureSupNorm(HashMap<X,Double> map1, HashMap<X,Double> map2, boolean abs)
 	{
-		assert(map1.size() == map2.size());
 		double value = 0;
 		Set<Entry<X,Double>> entries = map1.entrySet();
 		for (Entry<X,Double> entry : entries) {
@@ -222,7 +218,7 @@ public class PrismUtils
 					value = diff;
 				}
 			} else {
-				diff = Double.POSITIVE_INFINITY;
+				// Only check over common elements
 			}
 		}
 		return value;
@@ -234,9 +230,7 @@ public class PrismUtils
 	 */
 	public static double measureSupNorm(double[] d1, double[] d2, boolean abs)
 	{
-		int n = d1.length;
-		assert( n == d2.length);
-
+		int n = Math.min(d1.length, d2.length);
 		double value = 0;
 		if (abs) {
 			for (int i=0; i < n; i++) {
@@ -281,9 +275,6 @@ public class PrismUtils
 	 */
 	public static double measureSupNormInterval(double[] lower, double[] upper, boolean abs, PrimitiveIterator.OfInt indizes)
 	{
-		int n = lower.length;
-		assert( n== upper.length);
-
 		double value = 0;
 		while (indizes.hasNext()) {
 			int i = indizes.nextInt();
@@ -300,9 +291,7 @@ public class PrismUtils
 	 */
 	public static double measureSupNormInterval(double[] lower, double[] upper, boolean abs)
 	{
-		int n = lower.length;
-		assert( n== upper.length);
-
+		int n = Math.min(lower.length, upper.length);
 		double value = 0;
 		for (int i=0; i < n; i++) {
 			double diff = measureSupNormInterval(lower[i], upper[i], abs);