From e82b00b32568e761e6f400e28dcb5630395aee94 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sun, 5 Apr 2020 23:16:32 +0100
Subject: [PATCH] ParamResult and BigRational: Allow +Infinity as well as
 Infinity in result spec.

This makes it consistent with result testing for non-exact engines.
---
 prism/src/param/BigRational.java | 2 +-
 prism/src/param/ParamResult.java | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/prism/src/param/BigRational.java b/prism/src/param/BigRational.java
index 15a6c1a3..e0418920 100644
--- a/prism/src/param/BigRational.java
+++ b/prism/src/param/BigRational.java
@@ -184,7 +184,7 @@ public final class BigRational extends Number implements Comparable<BigRational>
 	 */
 	public BigRational(String string)
 	{
-		if (string.equals("Infinity") || string.equals("Inf")) {
+		if (string.equals("Infinity") || string.equals("+Infinity") || string.equals("Inf") || string.equals("+Inf")) {
 			this.num = new BigInteger("1");
 			this.den = new BigInteger("0");
 			return;
diff --git a/prism/src/param/ParamResult.java b/prism/src/param/ParamResult.java
index 2f39e95f..931dff01 100644
--- a/prism/src/param/ParamResult.java
+++ b/prism/src/param/ParamResult.java
@@ -132,7 +132,7 @@ public class ParamResult
 	{
 		Expression exprExpected = null;
 		try {
-			if (strExpected.equals("Infinity") || strExpected.equals("Inf")) {
+			if (strExpected.equals("Infinity") || strExpected.equals("+Infinity") || strExpected.equals("Inf") || strExpected.equals("+Inf")) {
 				exprExpected = new ExpressionLiteral(TypeDouble.getInstance(), BigRational.INF);
 			} else if (strExpected.equals("-Infinity") || strExpected.equals("-Inf")) {
 				exprExpected = new ExpressionLiteral(TypeDouble.getInstance(), BigRational.MINF);