From 004424bd3117f3f217adb6853a86c8d6b8e2d8cf 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.JasFunctionFactory.fromBigRational: handle special
 values directly

Before, the special values (Inf, -Inf, NaN) where implicitly passed
to JAS, now we just return the corresponding static singletons.
---
 prism/src/param/JasFunctionFactory.java | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/prism/src/param/JasFunctionFactory.java b/prism/src/param/JasFunctionFactory.java
index 46bc3f08..bb200859 100644
--- a/prism/src/param/JasFunctionFactory.java
+++ b/prism/src/param/JasFunctionFactory.java
@@ -133,6 +133,17 @@ final class JasFunctionFactory extends FunctionFactory {
 
 	@Override
 	public Function fromBigRational(BigRational from) {
+		if (from.isSpecial()) {
+			if (from.isInf())
+				return getInf();
+			else if (from.isMInf())
+				return getMInf();
+			else if (from.isNaN())
+				return getNaN();
+			else
+				throw new RuntimeException("Implementation error");
+		}
+
 		Quotient<BigInteger> result = jasQuotRing.fromInteger(from.getNum());
 		Quotient<BigInteger> den = jasQuotRing.fromInteger(from.getDen());
 		result = result.divide(den);