From 98d8e4cd724a67b9833ca07961c300c2b3d0ed68 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 13 Oct 2017 15:41:18 +0200
Subject: [PATCH] BigRational: parse nested fractionals from String (e.g.
 1/2/3)

---
 prism/src/param/BigRational.java | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/prism/src/param/BigRational.java b/prism/src/param/BigRational.java
index 90cb9c20..f1f7b748 100644
--- a/prism/src/param/BigRational.java
+++ b/prism/src/param/BigRational.java
@@ -193,10 +193,8 @@ public final class BigRational extends Number implements Comparable<BigRational>
 			this.den = new BigInteger("0");
 			return;
 		}
-		BigInteger num;
-		BigInteger den;
 		string = string.trim();
-		int slashIdx = string.indexOf('/');
+		int slashIdx = string.lastIndexOf('/');
 		if (slashIdx < 0) {
 			// decimal point notation
 			Double.parseDouble(string); // ensures correctness of format
@@ -225,7 +223,8 @@ public final class BigRational extends Number implements Comparable<BigRational>
 				int eInt = Integer.parseInt(eStr);
 				expo += eInt;
 			}
-			num = new BigInteger((negate ? "-" : "") + noDotCoeff);
+			BigInteger num = new BigInteger((negate ? "-" : "") + noDotCoeff);
+			BigInteger den;
 			BigInteger ten = BITEN;
 			if (expo == 0) {
 				den = BigInteger.ONE;
@@ -240,9 +239,14 @@ public final class BigRational extends Number implements Comparable<BigRational>
 			this.den = result.den;
 		} else {
 			// fractional
-			num = new BigInteger(string.substring(0, slashIdx));
-			den = new BigInteger(string.substring(slashIdx + 1, string.length()));
-			BigRational r = cancel(num, den);
+			if (slashIdx == 0 || slashIdx == string.length()-1) {
+				throw new NumberFormatException("Illegal fraction syntax");
+			}
+			// because we use lastIndexOf, we obtain left-associativity,
+			// i.e. a/b/c is interpreted as (a/b)/c
+			BigRational num = new BigRational(string.substring(0, slashIdx));
+			BigRational den = new BigRational(string.substring(slashIdx + 1, string.length()));
+			BigRational r = num.divide(den);
 			this.num = r.num;
 			this.den = r.den;
 			return;