From 06c914a476e2c1738e10118c76f41873388060c6 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 30 Jul 2014 15:19:34 +0000
Subject: [PATCH] Change visibility of some classes/methods in the param
 package to allow use from outside the package (and fix broken build).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9004 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/param/DagFunction.java       | 40 +++++++++++++-------------
 prism/src/param/JasFunction.java       | 10 +++++++
 prism/src/param/ParamModelChecker.java |  8 ++++++
 3 files changed, 38 insertions(+), 20 deletions(-)

diff --git a/prism/src/param/DagFunction.java b/prism/src/param/DagFunction.java
index ec70f6c5..4bb2866a 100644
--- a/prism/src/param/DagFunction.java
+++ b/prism/src/param/DagFunction.java
@@ -30,7 +30,7 @@ package param;
  * TODO implement completely
  * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
  */
-class DagFunction extends Function {
+public class DagFunction extends Function {
 	private DagFunctionFactory dagFactory;
 	private DagOperator num;
 	private DagOperator den;
@@ -40,7 +40,7 @@ class DagFunction extends Function {
 	final static int MINF = 2;
 	final static int NAN = 3;
 	
-	DagFunction(FunctionFactory factory, DagOperator num, DagOperator den) {
+	public DagFunction(FunctionFactory factory, DagOperator num, DagOperator den) {
 		super(factory);
 		dagFactory = (DagFunctionFactory) factory;
 		this.num = num;
@@ -48,18 +48,18 @@ class DagFunction extends Function {
 		this.type = NORMAL;
 	}
 	
-	DagFunction(FunctionFactory factory, int type) {
+	public DagFunction(FunctionFactory factory, int type) {
 		super(factory);
 		this.type = type;
 		num = null;
 		den = null;
 	}	
 
-	DagOperator getNum() {
+	public DagOperator getNum() {
 		return num;
 	}
 	
-	DagOperator getDen() {
+	public DagOperator getDen() {
 		return den;
 	}
 	
@@ -92,73 +92,73 @@ class DagFunction extends Function {
 
 	
 	@Override
-	Function add(Function other) {
+	public Function add(Function other) {
 		return dagFactory.add(this, (DagFunction) other);
 	}
 
 	@Override
-	Function negate() {
+	public Function negate() {
 		return dagFactory.negate(this);
 	}
 	
 	@Override
-	Function subtract(Function other) {
+	public Function subtract(Function other) {
 		return dagFactory.subtract(this, (DagFunction) other);
 	}
 
 	@Override
-	Function multiply(Function other) {
+	public Function multiply(Function other) {
 		return dagFactory.multiply(this, (DagFunction) other);
 	}
 
 	@Override
-	Function divide(Function other) {
+	public Function divide(Function other) {
 		return dagFactory.divide(this, (DagFunction) other);
 	}
 
 	@Override
-	Function star() {
+	public Function star() {
 		return dagFactory.star(this);
 	}
 
 	@Override
-	Function toConstraint() {
+	public Function toConstraint() {
 		return dagFactory.toConstraint(this);
 	}
 
 	@Override
-	BigRational evaluate(Point point, boolean cancel) {
+	public BigRational evaluate(Point point, boolean cancel) {
 		BigRational result = dagFactory.evaluate(this, point, cancel);
 		return result;
 	}
 
 	@Override
-	BigRational asBigRational() {
+	public BigRational asBigRational() {
 		return dagFactory.asBigRational(this);
 	}
 
 	@Override
-	boolean isNaN() {
+	public boolean isNaN() {
 		return type == NAN;
 	}
 
 	@Override
-	boolean isInf() {
+	public boolean isInf() {
 		return type == INF;
 	}
 
 	@Override
-	boolean isMInf() {
+	public boolean isMInf() {
 		return type == MINF;
 	}
 
 	@Override
-	boolean isOne() {
+	public boolean isOne() {
 		return dagFactory.isOne(this);
 	}
 
 	@Override
-	boolean isZero() {
+	public boolean isZero() {
 		return dagFactory.isZero(this);
 	}
 	
@@ -167,7 +167,7 @@ class DagFunction extends Function {
 		return dagFactory.toString(this);
 	}
 
-	int getType() {
+	public int getType() {
 		return type;
 	}
 }
diff --git a/prism/src/param/JasFunction.java b/prism/src/param/JasFunction.java
index b59f933f..2b06b567 100644
--- a/prism/src/param/JasFunction.java
+++ b/prism/src/param/JasFunction.java
@@ -182,6 +182,16 @@ final class JasFunction extends Function {
 		if (this.isNaN() || other.isNaN()) {
 			return factory.getNaN();
 		}
+		if (other.isZero()) {
+			if (this.isZero()) {
+				return factory.getNaN();
+			} else {
+				return factory.getInf();
+			}
+		}
+		if (this.isZero()) {
+			return factory.getZero();
+		}
 		return new JasFunction((JasFunctionFactory) factory, jas.divide(((JasFunction) other).jas), NORMAL);
 	}
 	
diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java
index 1451a3f0..d3e1a404 100644
--- a/prism/src/param/ParamModelChecker.java
+++ b/prism/src/param/ParamModelChecker.java
@@ -241,6 +241,14 @@ final public class ParamModelChecker extends PrismComponent
 		BitSet needStates = new BitSet(model.getNumStates());
 		needStates.set(0, model.getNumStates());
 		RegionValues vals = checkExpression(paramModel, expr, needStates);
+		mainLog.println(vals);
+		Function f = vals.getResult(0).getInitStateValueAsFunction();
+		int n = 100;
+		String s = "";
+		for (int i = 0; i < n; i++) {
+			BigRational br = f.evaluate(new param.Point(new BigRational[] {new BigRational(i, n)}));
+			s += " " + br.doubleValue();
+		}
 		timer = System.currentTimeMillis() - timer;
 		mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds.");