Read an infinite or undefined real

src/main/java/edu/uiowa/cs/clc/kind2/results/RealValue.java

@@ -9,17 +9,48 @@
 
 import com.google.gson.JsonElement;
 import com.google.gson.JsonObject;
+import edu.uiowa.cs.clc.kind2.Kind2Exception;
 
 import java.math.BigDecimal;
 import java.math.BigInteger;
 
 /**
  * The value of kind2 rational number.
+ *
+ * <p>Not every one of them is a number. Kind 2 reports an infinity and an
+ * undefined value as a fraction over a zero denominator, which is how a
+ * division by zero in the model reaches the counterexample: {@code 1/0} and
+ * {@code -1/0} for the infinities, {@code 0/0} for a value it could not
+ * determine. {@link #getKind} says which of the four a value is, and
+ * {@link #getValue} is the number only for a finite one.
  */
 public class RealValue extends Value
 {
   /**
-   * the value of the rational number.
+   * What a rational reported by Kind 2 turned out to be.
+   */
+  public enum Kind
+  {
+    /**
+     * A number, which {@link RealValue#getValue} returns.
+     */
+    FINITE,
+    /**
+     * Positive infinity, which Kind 2 writes as {@code 1/0}.
+     */
+    POSITIVE_INFINITY,
+    /**
+     * Negative infinity, which Kind 2 writes as {@code -1/0}.
+     */
+    NEGATIVE_INFINITY,
+    /**
+     * A value Kind 2 could not determine, which it writes as {@code 0/0}.
+     */
+    UNDEFINED
+  }
+
+  /**
+   * the value of the rational number, or null when it is not a number.
    */
   private final BigDecimal value;
   /**
@@ -30,6 +61,10 @@ public class RealValue extends Value
    * The denominator of the rational number
    */
   private final BigInteger denominator;
+  /**
+   * Which of the four kinds of rational this is.
+   */
+  private final Kind kind;
 
   /**
    * Constructs a real value from one Kind 2 stream value.
@@ -46,30 +81,131 @@ public RealValue(StepValue kind2StepValue, Type kind2Type, JsonElement jsonEleme
       JsonObject jsonObject = jsonElement.getAsJsonObject();
       numerator = new BigInteger(jsonObject.get(Labels.numerator).getAsString());
       denominator = new BigInteger(jsonObject.get(Labels.denominator).getAsString());
-      value = new BigDecimal(numerator).divide(new BigDecimal(denominator),
-          Result.getRealPrecision(), Result.getRealRoundingMode());
+      kind = kindOf(numerator, denominator);
+      // Dividing is only possible, and only means anything, for a finite one
+      value = kind == Kind.FINITE
+          ? new BigDecimal(numerator).divide(new BigDecimal(denominator),
+              Result.getRealPrecision(), Result.getRealRoundingMode())
+          : null;
     }
     else
     {
       value = jsonElement.getAsBigDecimal();
       numerator = value.unscaledValue();
       denominator = BigInteger.TEN.pow(value.scale());
+      kind = Kind.FINITE;
     }
   }
 
+  /**
+   * The kind a fraction denotes. A zero denominator carries an infinity whose
+   * sign is the sign of the numerator, or, with a zero numerator, a value
+   * Kind 2 could not determine.
+   */
+  private static Kind kindOf(BigInteger numerator, BigInteger denominator)
+  {
+    if (denominator.signum() != 0)
+    {
+      return Kind.FINITE;
+    }
+    if (numerator.signum() > 0)
+    {
+      return Kind.POSITIVE_INFINITY;
+    }
+    if (numerator.signum() < 0)
+    {
+      return Kind.NEGATIVE_INFINITY;
+    }
+    return Kind.UNDEFINED;
+  }
+
+  /**
+   * Returns which of the four kinds of rational this value is.
+   *
+   * @return the kind of this value
+   */
+  public Kind getKind()
+  {
+    return kind;
+  }
+
+  /**
+   * Returns whether this value is a number, and so whether
+   * {@link #getValue} returns one.
+   *
+   * @return {@code true} if this value is finite
+   */
+  public boolean isFinite()
+  {
+    return kind == Kind.FINITE;
+  }
+
   /**
    * Returns the value of the rational number.
    *
    * @return the value of the rational number.
+   * @throws Kind2Exception if this value is not a number, which
+   *         {@link #isFinite} tells apart beforehand
    */
   public BigDecimal getValue()
   {
+    if (value == null)
+    {
+      throw new Kind2Exception(
+          "This value is " + kind + " rather than a number, so it has no "
+              + "decimal value. Kind 2 reports it as " + this
+              + ". Use isFinite() to tell the two apart, or getDoubleValue().");
+    }
     return value;
   }
 
+  /**
+   * Returns this value as a {@code double}, which, unlike a
+   * {@link BigDecimal}, can carry an infinity and a value Kind 2 could not
+   * determine. A finite one is rounded to the nearest {@code double}.
+   *
+   * @return this value as a {@code double}
+   */
+  public double getDoubleValue()
+  {
+    switch (kind)
+    {
+      case POSITIVE_INFINITY:
+        return Double.POSITIVE_INFINITY;
+      case NEGATIVE_INFINITY:
+        return Double.NEGATIVE_INFINITY;
+      case UNDEFINED:
+        return Double.NaN;
+      default:
+        return value.doubleValue();
+    }
+  }
+
+  /**
+   * Returns the numerator of this value expressed as a fraction.
+   *
+   * @return the numerator of this value
+   */
+  public BigInteger getNumerator()
+  {
+    return numerator;
+  }
+
+  /**
+   * Returns the denominator of this value expressed as a fraction, which is
+   * zero for every value that is not a number.
+   *
+   * @return the denominator of this value
+   */
+  public BigInteger getDenominator()
+  {
+    return denominator;
+  }
+
   @Override
   public String toString()
   {
-    return value.toString();
+    // What Kind 2 itself prints for these, in its plain text and its XML
+    return value == null ? numerator + "/" + denominator : value.toString();
   }
 }

src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java

@@ -9,14 +9,19 @@
 package edu.uiowa.cs.clc.kind2.results;
 
 import java.io.IOException;
+import java.math.BigDecimal;
 import java.math.BigInteger;
 import java.math.RoundingMode;
 import java.nio.file.Files;
 import java.nio.file.Paths;
 import java.util.Arrays;
 import java.util.List;
 
+import edu.uiowa.cs.clc.kind2.Kind2Exception;
+
 import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertThrows;
 import static org.junit.jupiter.api.Assertions.assertNotNull;
 import static org.junit.jupiter.api.Assertions.assertNull;
 import static org.junit.jupiter.api.Assertions.assertTrue;
@@ -664,4 +669,53 @@ void machineIntegerCounterExample()
     IntValue wide = (IntValue) streams.get(2).getStepValues().get(0).getKind2Value();
     assertEquals(new BigInteger("16777215"), wide.getValue());
   }
+  /**
+   * A counterexample holding the rationals that are not numbers. A division
+   * by zero in the model reaches it as a fraction over a zero denominator,
+   * and reading one used to throw out of the constructor of {@link
+   * RealValue} and take the whole result with it.
+   */
+  @Test
+  void realValuesThatAreNotNumbers()
+  {
+    String json = "[{'objectType' : 'log','level' : 'info','source' : 'parse','value' : 'kind2 v3.0.0'},{'objectType' : 'analysisStart','top' : 'bla','concrete' : [],'abstract' : [],'assumptions' : []},{'objectType' : 'property','name' : 'InvProp[l18c3]','source' : 'PropAnnot','file' : './examples/div.lus','line' : 18,'column' : 3,'runtime' : {'unit' : 'sec', 'timeout' : false, 'value' : 0.010},'k' : 0,'answer' : {'source' : 'bmc', 'value' : 'falsifiable'},'counterExample' :[{'blockType' : 'node','name' : 'bla','streams' :[{'name' : 'i','type' : 'real','class' : 'input','instantValues' : [[0, {'num': 0, 'den': 1}]]},{'name' : 'inf_pos','type' : 'real','class' : 'local','instantValues' : [[0, {'num': 1, 'den': 0}]]},{'name' : 'inf_neg','type' : 'real','class' : 'local','instantValues' : [[0, {'num': -1, 'den': 0}]]},{'name' : 'inf_p_div_n','type' : 'real','class' : 'local','instantValues' : [[0, {'num': 0, 'den': 0}]]}]}]},{'objectType' : 'analysisStop'}]";
+
+    Result result = Result.analyzeJsonResult(json);
+    assertNotNull(result.getRoot());
+
+    Property property = result.getRoot().getAnalyses().get(0).getFalsifiedProperties().get(0);
+    List<Stream> streams = property.getCounterExample().getTopNode().getStreams();
+
+    RealValue finite = realValueOf(streams.get(0));
+    assertEquals(RealValue.Kind.FINITE, finite.getKind());
+    assertTrue(finite.isFinite());
+    assertEquals(0, BigDecimal.ZERO.compareTo(finite.getValue()));
+    assertEquals(0.0, finite.getDoubleValue());
+
+    RealValue positive = realValueOf(streams.get(1));
+    assertEquals(RealValue.Kind.POSITIVE_INFINITY, positive.getKind());
+    assertFalse(positive.isFinite());
+    assertEquals("1/0", positive.toString());
+    assertEquals(Double.POSITIVE_INFINITY, positive.getDoubleValue());
+    assertThrows(Kind2Exception.class, positive::getValue);
+
+    RealValue negative = realValueOf(streams.get(2));
+    assertEquals(RealValue.Kind.NEGATIVE_INFINITY, negative.getKind());
+    assertEquals("-1/0", negative.toString());
+    assertEquals(Double.NEGATIVE_INFINITY, negative.getDoubleValue());
+
+    RealValue undefined = realValueOf(streams.get(3));
+    assertEquals(RealValue.Kind.UNDEFINED, undefined.getKind());
+    assertEquals("0/0", undefined.toString());
+    assertTrue(Double.isNaN(undefined.getDoubleValue()));
+
+    // The fraction Kind 2 reported is readable whichever kind it is
+    assertEquals(BigInteger.ONE, positive.getNumerator());
+    assertEquals(BigInteger.ZERO, positive.getDenominator());
+  }
+
+  private static RealValue realValueOf(Stream stream)
+  {
+    return (RealValue) stream.getStepValues().get(0).getKind2Value();
+  }
 }