From 3d5e75627d83022afa7f2f01f3bdc2a9606541f6 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 13 Oct 2017 15:41:18 +0200 Subject: [PATCH] DefinedConstant/UndefinedConstants: support exact constants (BigRational) Supports an exact mode where constants (and experiments with a range of constants) can be defined using exact arithmetic (i.e., via BigRational) --- prism/src/prism/DefinedConstant.java | 167 +++++++++++++++++++----- prism/src/prism/UndefinedConstants.java | 11 +- 2 files changed, 146 insertions(+), 32 deletions(-) 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)