diff --git a/prism/src/prism/DefinedConstant.java b/prism/src/prism/DefinedConstant.java
index 18e1648a..ad0069a1 100644
--- a/prism/src/prism/DefinedConstant.java
+++ b/prism/src/prism/DefinedConstant.java
@@ -27,6 +27,7 @@
package prism;
+import param.BigRational;
import parser.type.*;
/**
@@ -80,14 +81,22 @@ public class DefinedConstant
return (low != null);
}
- /** Define the constant (by passing in strings). */
-
- public void define(String sl, String sh, String ss) throws PrismException
+ /**
+ * Define the constant (by passing in strings).
+ *
+ * If {@code exact} is true, BigRationals are used for real values,
+ * otherwise double arithmetic is used.
+ */
+ public void define(String sl, String sh, String ss, boolean exact) throws PrismException
{
if (type instanceof TypeInt) {
defineInt(sl, sh, ss);
- }else if (type instanceof TypeDouble) {
- defineDouble(sl, sh, ss);
+ } else if (type instanceof TypeDouble) {
+ if (exact) {
+ defineBigRational(sl, sh, ss);
+ } else {
+ defineDouble(sl, sh, ss);
+ }
} else if (type instanceof TypeBool) {
defineBoolean(sl, sh, ss);
} else {
@@ -212,7 +221,65 @@ public class DefinedConstant
high = new Double(dh);
step = new Double(ds);
}
-
+
+ public void defineBigRational(String sl, String sh, String ss) throws PrismException
+ {
+ BigRational r, rl, rh, rs;
+
+ // parse low value
+ try {
+ rl = BigRational.from(sl);
+ }
+ catch (NumberFormatException e) {
+ throw new PrismException("Value " + sl + " for constant " + name + " is not a valid rational number");
+ }
+ // if no high value given, use low value, default step is 1.0
+ if (sh == null) {
+ rh = rl;
+ rs = BigRational.from(1);
+ }
+ else {
+ // parse high value
+ try {
+ rh = BigRational.from(sh);
+ }
+ catch (NumberFormatException e) {
+ throw new PrismException("Value " + sh + " for constant " + name + " is not a valid rational number");
+ }
+ if (rh.lessThan(rl)) throw new PrismException("Low value "+rl+" for constant " + name + " is higher than the high value "+rh);
+ if (ss == null) {
+ // default step is 1.0
+ rs = BigRational.from(1);
+ }
+ else {
+ // parse step
+ try {
+ rs = BigRational.from(ss);
+ }
+ catch (NumberFormatException e) {
+ throw new PrismException("Value " + ss + " for constant " + name + " is not a valid double");
+ }
+ if (rs.isZero()) throw new PrismException("Step value for constant " + name + " cannot be zero");
+ if (rs.lessThan(BigRational.ZERO)) throw new PrismException("Step value for constant " + name + " must be positive");
+ if (rs.greaterThan(rh.subtract(rl))) throw new PrismException("Step value "+rs+" for constant " + name + " is bigger than the difference between "+rl+" and "+rh);
+ }
+ }
+ // compute num steps
+ numSteps = 0;
+ BigRational rhNew = rh;
+ for (r = rl; r.lessThanEquals(rh); r = rl.add(rs.multiply(numSteps)))
+ {
+ numSteps++;
+ rhNew = r;
+ }
+ // store 'actual' value for high
+ rh = rhNew;
+ // store
+ low = rl;
+ high = rh;
+ step = rs;
+ }
+
public void defineBoolean(String sl, String sh, String ss) throws PrismException
{
// parse value (low)
@@ -261,20 +328,39 @@ public class DefinedConstant
}
// double
else if (type instanceof TypeDouble) {
- dl = ((Double)low).doubleValue();
- dh = ((Double)high).doubleValue();
- ds = ((Double)step).doubleValue();
- dv = ((Double)value).doubleValue();
- // if possible, increment
- int index = getValueIndex(value) + 1;
- dv = dl + index * ds;
- if (dv <= dh + DOUBLE_PRECISION_CORRECTION * ds) {
- value = new Double(dv);
- }
- // otherwise, reset to low value, note overflow
- else {
- value = low;
- overflow = true;
+ if (low instanceof BigRational) {
+ BigRational rl = (BigRational) low;
+ BigRational rh = (BigRational) high;
+ BigRational rs = (BigRational) step;
+ BigRational rv = (BigRational) value;
+ // if possible, increment
+ int index = getValueIndex(value) + 1;
+ rv = rl.add(rs.multiply(index));
+ if (rv.lessThanEquals(rh)) {
+ value = rv;
+ }
+ // otherwise, reset to low value, note overflow
+ else {
+ value = low;
+ overflow = true;
+ }
+ } else {
+ // double arithmetic
+ dl = ((Double)low).doubleValue();
+ dh = ((Double)high).doubleValue();
+ ds = ((Double)step).doubleValue();
+ dv = ((Double)value).doubleValue();
+ // if possible, increment
+ int index = getValueIndex(value) + 1;
+ dv = dl + index * ds;
+ if (dv <= dh + DOUBLE_PRECISION_CORRECTION * ds) {
+ value = new Double(dv);
+ }
+ // otherwise, reset to low value, note overflow
+ else {
+ value = low;
+ overflow = true;
+ }
}
}
// boolean
@@ -315,12 +401,21 @@ public class DefinedConstant
}
// double
else if (type instanceof TypeDouble) {
- dl = ((Double)low).doubleValue();
- ds = ((Double)step).doubleValue();
- dv = dl;
- //for (i = 0; i < j; i++) dv += ds;
- dv = dl + j * ds;
- return new Double(dv);
+ if (low instanceof BigRational) {
+ BigRational rl = (BigRational)low;
+ BigRational rs = (BigRational)low;
+ BigRational rv;
+ // rv = rl + j*rs
+ rv = rl.add(rs.multiply(j));
+ return rv;
+ } else {
+ dl = ((Double)low).doubleValue();
+ ds = ((Double)step).doubleValue();
+ dv = dl;
+ //for (i = 0; i < j; i++) dv += ds;
+ dv = dl + j * ds;
+ return new Double(dv);
+ }
}
// boolean (case should be redundant)
else if (type instanceof TypeBool) {
@@ -350,10 +445,22 @@ public class DefinedConstant
}
// double
else if (type instanceof TypeDouble) {
- dl = ((Double)low).doubleValue();
- ds = ((Double)step).doubleValue();
- dv = ((Double)v).doubleValue();
- return (int)Math.round((dv-dl)/ds);
+ if (low instanceof BigRational) {
+ BigRational rl = (BigRational) low;
+ BigRational rs = (BigRational) step;
+ BigRational rv = (BigRational) value;
+ BigRational index = (rv.subtract(rl)).divide(rs);
+ try {
+ return index.toInt();
+ } catch (PrismLangException e) {
+ throw new IllegalArgumentException("Can not compute value index, out of range: " + e);
+ }
+ } else {
+ dl = ((Double)low).doubleValue();
+ ds = ((Double)step).doubleValue();
+ dv = ((Double)v).doubleValue();
+ return (int)Math.round((dv-dl)/ds);
+ }
}
// boolean (case should be redundant)
else if (type instanceof TypeBool) {
diff --git a/prism/src/prism/UndefinedConstants.java b/prism/src/prism/UndefinedConstants.java
index 29825a1e..3fdce314 100644
--- a/prism/src/prism/UndefinedConstants.java
+++ b/prism/src/prism/UndefinedConstants.java
@@ -54,6 +54,8 @@ public class UndefinedConstants
private List props = null;
// just get constants from labels (in properties file)?
private boolean justLabels = false;
+ // computation / evaluation of constants via double or exact arithmetic?
+ private boolean exact = false;
// info about constants
private int mfNumConsts = 0;
@@ -150,6 +152,11 @@ public class UndefinedConstants
this.justLabels = justLabels;
}
+ public void setExactMode(boolean exact)
+ {
+ this.exact = exact;
+ }
+
/**
* Initialise this UndefinedConstants object:
* determine which constants are undefined and then set up data structures.
@@ -503,13 +510,13 @@ public class UndefinedConstants
if (index != -1) {
// const is in modules file
overwrite = (mfConsts.get(index).isDefined());
- mfConsts.get(index).define(sl, sh, ss);
+ mfConsts.get(index).define(sl, sh, ss, exact);
} else {
index = getPFConstIndex(name);
if (index != -1) {
// const is in properties file
overwrite = (pfConsts.get(index).isDefined());
- pfConsts.get(index).define(sl, sh, ss);
+ pfConsts.get(index).define(sl, sh, ss, exact);
} else {
// If we are required to use all supplied const values, check for this
// (by default we don't care about un-needed or non-existent const values)