From 8915bcd7800835358a61640c94473c2a7db3454e Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 22 Sep 2026 12:53:52 -0500 Subject: [PATCH] Read an infinite or undefined real Not every rational Kind 2 reports is a number. Its decimal type is type t = | InfPos | InfNeg | Undef | N of Num.num and it writes the first three as a fraction over a zero denominator: 1/0 and -1/0 for the infinities, 0/0 for a value it could not determine. That is how a division by zero in the model reaches a counterexample, alongside the warning Kind 2 prints about it, and the plain text and the XML render them that way too. RealValue divided the numerator by the denominator as it was constructed, so one of these threw ArithmeticException out of the constructor. Values are built while the Result is, so a single undefined value in a single stream destroyed the whole result for a model Kind 2 had analysed and reported on. A rational now says which of the four it is. `getKind` and `isFinite` tell them apart, `getValue` returns the number for a finite one and otherwise throws a Kind2Exception naming what it holds, and `getDoubleValue` gives all four, since a double carries an infinity and a NaN where a BigDecimal carries neither. `toString` renders the three as Kind 2 does, so a counterexample reads the same through this API as through Kind 2's own output. The numerator and the denominator, which had no accessors at all, are readable too. Co-Authored-By: Claude Opus 5 (1M context) --- .../uiowa/cs/clc/kind2/results/RealValue.java | 144 +++++++++++++++++- .../clc/kind2/results/Kind2ResultTests.java | 54 +++++++ 2 files changed, 194 insertions(+), 4 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/RealValue.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/RealValue.java index 51de0b0..fa04062 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/RealValue.java +++ b/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. + * + *

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(); } } diff --git a/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java b/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java index 5fc2569..277890c 100644 --- a/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java +++ b/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java @@ -9,6 +9,7 @@ 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; @@ -16,7 +17,11 @@ 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 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(); + } }