s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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)
master
Joachim Klein 8 years ago
committed by Dave Parker
parent
6f3b25d0b8
commit
3d5e75627d
2 changed files with 146 additions and 32 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 167
      prism/src/prism/DefinedConstant.java
  2. 11
      prism/src/prism/UndefinedConstants.java

167
prism/src/prism/DefinedConstant.java
View File

@ -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).
* <br>
* 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) {

11
prism/src/prism/UndefinedConstants.java
View File

@ -54,6 +54,8 @@ public class UndefinedConstants
private List<Property> 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)

Write Preview
Loading…
Cancel
Save