Browse Source

ParamResult and BigRational: Allow +Infinity as well as Infinity in result spec.

This makes it consistent with result testing for non-exact engines.
accumulation-v4.7
Dave Parker 6 years ago
parent
commit
e82b00b325
  1. 2
      prism/src/param/BigRational.java
  2. 2
      prism/src/param/ParamResult.java

2
prism/src/param/BigRational.java

@ -184,7 +184,7 @@ public final class BigRational extends Number implements Comparable<BigRational>
*/ */
public BigRational(String string) public BigRational(String string)
{ {
if (string.equals("Infinity") || string.equals("Inf")) {
if (string.equals("Infinity") || string.equals("+Infinity") || string.equals("Inf") || string.equals("+Inf")) {
this.num = new BigInteger("1"); this.num = new BigInteger("1");
this.den = new BigInteger("0"); this.den = new BigInteger("0");
return; return;

2
prism/src/param/ParamResult.java

@ -132,7 +132,7 @@ public class ParamResult
{ {
Expression exprExpected = null; Expression exprExpected = null;
try { try {
if (strExpected.equals("Infinity") || strExpected.equals("Inf")) {
if (strExpected.equals("Infinity") || strExpected.equals("+Infinity") || strExpected.equals("Inf") || strExpected.equals("+Inf")) {
exprExpected = new ExpressionLiteral(TypeDouble.getInstance(), BigRational.INF); exprExpected = new ExpressionLiteral(TypeDouble.getInstance(), BigRational.INF);
} else if (strExpected.equals("-Infinity") || strExpected.equals("-Inf")) { } else if (strExpected.equals("-Infinity") || strExpected.equals("-Inf")) {
exprExpected = new ExpressionLiteral(TypeDouble.getInstance(), BigRational.MINF); exprExpected = new ExpressionLiteral(TypeDouble.getInstance(), BigRational.MINF);

Loading…
Cancel
Save