From 777af75ee8c6eb53777ea6d9aae35ffe93fe8a14 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 19 Aug 2016 09:56:22 +0000
Subject: [PATCH] param.Dag: handle special functions (+/-inf, NaN) in
 fromBigRational and asBigRational

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11650 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/param/DagFunction.java        | 12 +++++++++++-
 prism/src/param/DagFunctionFactory.java | 12 ++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/prism/src/param/DagFunction.java b/prism/src/param/DagFunction.java
index 265f37b0..64ed411a 100644
--- a/prism/src/param/DagFunction.java
+++ b/prism/src/param/DagFunction.java
@@ -134,7 +134,17 @@ public class DagFunction extends Function {
 
 	@Override
 	public BigRational asBigRational() {
-		return dagFactory.asBigRational(this);
+		switch (type) {
+		case NORMAL:
+			return dagFactory.asBigRational(this);
+		case NAN:
+			return BigRational.NAN;
+		case INF:
+			return BigRational.INF;
+		case MINF:
+			return BigRational.MINF;
+		}
+		throw new RuntimeException("Illegal type");
 	}
 
 	@Override
diff --git a/prism/src/param/DagFunctionFactory.java b/prism/src/param/DagFunctionFactory.java
index a5fd2999..411f0bde 100644
--- a/prism/src/param/DagFunctionFactory.java
+++ b/prism/src/param/DagFunctionFactory.java
@@ -221,6 +221,18 @@ class DagFunctionFactory extends FunctionFactory {
 	
 	@Override
 	Function fromBigRational(BigRational bigRat) {
+		if (bigRat.isSpecial()) {
+			if (bigRat.isNaN()) {
+				return getNaN();
+			} else if (bigRat.isInf()) {
+				return getInf();
+			} else if (bigRat.isMInf()) {
+				return getMInf();
+			} else {
+				throw new RuntimeException("Unknown special value");
+			}
+		}
+		// normal:
 		bigRat = bigRat.cancel();
 		DagOperator num = new Number(bigRat.getNum());
 		num = makeUnique(num);