Read an infinite or undefined real

[daniel-larraz]

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 —
{"num": 1, "den": 0} and {"num": -1, "den": 0} for the infinities,
{"num": 0, "den": 0} for a value it could not determine. That is how a
division by zero in the model reaches a counterexample, together with the
warning Kind 2 prints about it, and its plain text and XML render the three
as 1/0, -1/0 and 0/0.

RealValue divided the numerator by the denominator as it was constructed:

value = new BigDecimal(numerator).divide(new BigDecimal(denominator), …);

which throws ArithmeticException: / by zero on any of them. Values are
built while the Result is, so one undefined value in one stream destroyed
the whole result for a model Kind 2 had analysed and reported on:

java.lang.ArithmeticException: / by zero
  at ...results.RealValue.<init>(RealValue.java:49)
  at ...results.Value.getKind2Value(Value.java:90)
  at ...results.StepValue.<init>(StepValue.java:47)
  …
  at ...results.Result.initialize(Result.java:240)

What changes

A rational now says which of the four kinds it is, rather than assuming it is
a number:

getKind()	FINITE, POSITIVE_INFINITY, NEGATIVE_INFINITY or UNDEFINED
isFinite()	whether getValue() will give a number
getValue()	the BigDecimal for a finite one; otherwise throws a Kind2Exception naming what it holds
getDoubleValue()	all four: a double carries an infinity and a NaN where a BigDecimal carries neither
getNumerator(), getDenominator()	the fraction Kind 2 reported, which had no accessors at all
toString()	1/0, -1/0, 0/0 for the three, as Kind 2 itself prints them

getValue() throws rather than returning null on purpose: a null
BigDecimal surfaces as a NullPointerException somewhere away from the
cause, where the exception says what the value is and how to ask about it
first. Nothing can depend on the old behaviour, since the old behaviour was
to throw out of the constructor and lose the result.

toString() matching Kind 2 means a counterexample reads the same through
this API as through Kind 2's own output, and the table in SubNode, which
sizes its columns from toString().length(), keeps working.

The kind is a nested RealValue.Kind rather than another top-level enum in
results: unlike PropertyType or LogLevel it has no meaning away from
the class it describes.

Before and after, on the same counterexample

tests/regression/falsifiable/test-div-by-zero.lus in the Kind 2 tree
produces all three kinds. Reading its output:

  API as on main:        FAIL java.lang.ArithmeticException: / by zero
  API with this change:  OK

and the counterexample it now yields, beside what Kind 2 prints for the same
run:

  i                  = 0.00     kind=FINITE            double=0.0
  out                = -7.00    kind=FINITE            double=-7.0
  inf_pos            = 1/0      kind=POSITIVE_INFINITY double=Infinity
  inf_neg            = -1/0     kind=NEGATIVE_INFINITY double=-Infinity
  inf_p_div_n        = 0/0      kind=UNDEFINED         double=NaN
  inf_p_sub_n        = 1/0      kind=POSITIVE_INFINITY double=Infinity
  one_div_inf_p      = 0.00     kind=FINITE            double=0.0
  inf_p_sum_inf_n    = 0/0      kind=UNDEFINED         double=NaN

Tests

realValuesThatAreNotNumbers reads a counterexample holding a finite value
and all three of the others, and checks the kind, isFinite, toString,
getDoubleValue, the fraction, and that getValue throws for an infinity.

The existing 33 result tests and 10 pretty printer tests still pass,
javadoc -Xdoclint:all is clean over the main sources, and it compiles at
the Java 8 language level CI builds with.

Every model in the Kind 2 regression tree (639) now reads through
Result.analyzeJsonResult — the first time that has been true. This was
the last one failing, and the one named as unrelated in #25 and #26.

🤖 Generated with Claude Code