From a6e44588052b02498965c9a76102d7d59ed7292a Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Sun, 5 Apr 2020 22:20:07 +0200
Subject: [PATCH] param.BigRational: Handle division by zero explicitly

Ensures that we get consistent behaviour with the other engines (IEEE floating-point semantics).
---
 prism/src/param/BigRational.java | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/prism/src/param/BigRational.java b/prism/src/param/BigRational.java
index 2bdd9411..15a6c1a3 100644
--- a/prism/src/param/BigRational.java
+++ b/prism/src/param/BigRational.java
@@ -435,6 +435,19 @@ public final class BigRational extends Number implements Comparable<BigRational>
 		if (other.isInf() || other.isMInf()) {
 			return NAN;
 		}
+
+		if (other.isZero()) {
+			if (this.isZero() || this.isNaN()) {
+				return BigRational.NAN;
+			} else {
+				if (this.signum() > 0) {
+					return BigRational.INF;
+				} else {
+					return BigRational.MINF;
+				}
+			}
+		}
+
 		BigRational inverseOther = new BigRational(other.den, other.num, cancel);
 		return multiply(inverseOther, cancel);
 	}