From 1f9fb4d505cb7b78fcb4ac8f8adec8110c175cc4 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 9 Sep 2016 08:35:13 +0000
Subject: [PATCH] BigRational: When canceling, preserve NaN instead of
 converting to ZERO

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

diff --git a/prism/src/param/BigRational.java b/prism/src/param/BigRational.java
index 3131c1f9..a9791f6a 100644
--- a/prism/src/param/BigRational.java
+++ b/prism/src/param/BigRational.java
@@ -126,8 +126,12 @@ public final class BigRational implements Comparable<BigRational>
 		}
 		if (cancel) {
 			if (num.equals(BigInteger.ZERO)) {
-				num = BigInteger.ZERO;
-				den = BigInteger.ONE;
+				if (!den.equals(BigInteger.ZERO)) {
+					// not NaN (= 0/0), so this is a real zero:
+					// normalise by setting denominator to 1
+					num = BigInteger.ZERO;
+					den = BigInteger.ONE;
+				}
 			} else {
 				BigInteger gcd = num.gcd(den);
 				num = num.divide(gcd);