Read algebraic datatype values by daniel-larraz · Pull Request #25 · kind2-mc/kind2-java-api

daniel-larraz · 2026-09-22T02:12:51Z

A stream of an algebraic datatype had no type of its own here. "datatype"
fell through the switch in Type.getType to its default, which treats an
unrecognised type name as an enumeration, and an enumeration's value is read
with getAsString(). Kind 2 writes a constructor applied to its fields as an
object, so reading a counterexample over a datatype threw
UnsupportedOperationException: JsonObject out of EnumValue, and since the
values are built while the Result is, it took the whole result with it:

java.lang.UnsupportedOperationException: JsonObject
  at ...results.EnumValue.<init>(EnumValue.java:29)
  at ...results.Value.getKind2Value(Value.java:110)
  at ...results.StepValue.<init>(StepValue.java:47)
  at ...results.Stream.<init>(Stream.java:70)
  at ...results.SubNode.<init>(SubNode.java:75)
  at ...results.CounterExample.<init>(CounterExample.java:45)
  at ...results.Property.<init>(Property.java:125)
  at ...results.Result.initialize(Result.java:240)

What changes

Datatype (a Type) reports the name and the constructors of the datatype,
so a stream of one reads as List rather than as the literal word
datatype. DatatypeValue (a Value) carries the constructor the value was
built with and the fields it was applied to, and prints as Cons(1, Nil), or
as Nil for a constructor that takes none.

Kind 2 does not name the types of a constructor's fields in its output, so
Value.getFieldType takes the type of a field from the shape of its json —
an object naming a constructor is another datatype value, an object with a
numerator and a denominator is a real, an array is an array, and a primitive
is whichever of a Boolean, a number or a name it holds. The field is then
read through the same getKind2Value dispatch as every other value, rather
than through a second copy of that logic.

Compatibility

Kind 2 releases up to 3.0.0 wrote a constructor taking no fields as a bare
name — [0, Nil] — which is not a JSON value. gson parses leniently and read
it as the string "Nil", so it worked by accident; a strict parser rejects
the document, which is kind2-mc/kind2#1467. kind2-mc/kind2#1549 fixes that by
writing it as a constructor with an empty field list, like any other.

DatatypeValue accepts both forms, so this reads the output of Kind 2
releases before and after that fix identically. Verified over every model in
the Kind 2 regression tree (639 models), against Kind 2 binaries built before
and after that PR — the number of models whose result this API cannot read:

	Kind 2 before #1549	Kind 2 after #1549
this API, as released	4	9
this API, with this PR	3	1

Reading the four cells:

as released, before — msg_self_enc.lus throws
UnsupportedOperationException on a constructor with fields, which is the
bug this PR fixes. gen_call_in_type_decl.lus and
output_escaped_names.lus throw JsonSyntaxException: Kind 2 truncated
the one document and wrote an invalid escape in the other, both fixed by
#1549 rather than here.
as released, after — the same, plus the seven models whose
counterexample holds a constructor with no fields. Those read before only
because gson leniently took the bare name for a string; #1549 makes it an
object, which EnumValue cannot read. Without this PR, #1549 would
regress them.
with this PR, before — the two JsonSyntaxException models, which
need the Kind 2 fix.
with this PR, after — nothing datatype-related left.

The model failing in all four cells is test-div-by-zero.lus, which is
unrelated to datatypes and untouched here: Kind 2 reports a real that came
from a division by zero as {"num": 1, "den": 0}, and RealValue divides
by that denominator, so it throws ArithmeticException: / by zero. Worth its
own issue.

Counterexamples that only ever worked by gson's leniency now read properly,
and ones with a constructor that does take fields read at all for the first
time:

  l : List = [Nil]          (threw IllegalStateException before)
  m : Msg  = [Atomic(0)]    (threw UnsupportedOperationException before)
  n : Nat  = [Zero]

Tests

Two cases in Kind2ResultTests, over a counterexample holding both Nil and
Cons(1, Nil): one on the current output shape, one on the bare-name shape
older Kind 2 releases wrote. The existing 30 result tests and 10 pretty
printer tests still pass, and javadoc -Xdoclint:all is clean over the main
sources.

Compiles at the Java 8 language level, which is what CI builds with.

Follow-ups, not in this PR

Once this is released, the language server and the vscode extension only need
a dependency bump — neither has any datatype handling of its own, and
everything they send onward is re-serialized by this API.

Two other type names still fall through to the enumeration default:
"abstr", for an uninterpreted sort, and "adt", for a reconstructed ADT
stream. Both happen to work, because their values are names, but neither
reports a useful type. Worth their own change.

🤖 Generated with Claude Code

A stream of an algebraic datatype had no type of its own here: "datatype" fell through to the default of Type.getType and became an Enum, whose value is read with getAsString(). Kind 2 writes a constructor applied to its fields as {"constructor": ..., "args": [...]}, so reading a counterexample over a datatype threw UnsupportedOperationException from EnumValue and took the whole Result with it. This adds Datatype and DatatypeValue, so such a stream reports the name and the constructors of its datatype, and its values carry the constructor they were built with and the fields it was applied to. Kind 2 does not name the types of a constructor's fields in its output, so a field is read as the type its json shape gives it, through the dispatch the other values use. Kind 2 releases up to 3.0.0 wrote a constructor taking no fields as a bare name rather than as a constructor with an empty field list, which gson read leniently as a string. That form is still understood, so the output of those releases reads the same as the output of the release that fixed it (kind2-mc/kind2#1549). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Closes #1467. `--json` output is not parseable when a property expression pretty-prints across more than one line: the `"expr"` field embeds the raw newlines. The field was written into the document with no escaping at all, and the helper that should have done it would not have been enough on its own — so this PR fixes the escaping in both machine-readable formats, and the ways the trace printers had of writing something neither format could read back. Checking the fix over the regression tree turned up eleven more models whose JSON no consumer could parse and twenty-three whose XML was not well-formed. All of them are fixed here. Every model in the tree now produces parseable JSON and well-formed XML. ## What changes ### The escapers `escape_json_string` escaped none of what it claimed to. `Str.global_replace` reads `\\` in a replacement template as one literal backslash, so the backslash rule was a no-op; quotes were rewritten to `'` rather than escaped, and tabs, carriage returns and the rest of the control range were passed through raw. It is now a single pass that escapes `"`, `\`, `\b`, `\f`, `\n`, `\r`, `\t` and `\u00xx`, leaving bytes at or above `0x80` alone so UTF-8 passes through as itself. `escape_xml_string` did not escape quotes, so a property named with one ended its attribute early. It also substituted `&` last, so the ampersands its own `<` and `>` introduced were escaped again: a `<` in a log message came out as `&lt;`. It is now a single pass as well. | | Before | After | |---|---|---| | `C:\models\top.lus` in JSON | `C:\models\top.lus` (decodes back with a tab and a newline) | `C:\\models\\top.lus` | | `a "quoted" name` in JSON | `a 'quoted' name` | `a \"quoted\" name` | | a tab in a log message | raw, not legal in a JSON string | `\t` | | `a "quoted" name` in XML | `name="a "quoted" name"` | `name="a "quoted" name"` | | `<` in a log message | `&lt;` | `<` | Every name, file path and scope written into either format now goes through the escaper for that format. That covers the `name`, `top`, `concrete` and `abstract` attributes, which used to take the name of a monomorphized node raw — and that name carries its type arguments in angle brackets, so `<AnalysisStart concrete="O<int>,N<int>">` was not well-formed. ### Values and types in a trace - **A stream of an uninterpreted sort** reported its type as the bare sort name. In XML that made the name an attribute of its own with no value: `<Stream name="init" COUNTER class="input">`. In JSON it was an unquoted `"name" : COUNTER`. Both schemas already describe the right shape (`abstrName`, and a `typeInfo.name` string), and the printers now match it. - **A value of an uninterpreted sort** (`COUNTER.0`) was written bare. Any value JSON has no literal of its own for is now written as a string. - **A constructor that takes no fields** is a constant rather than an application, so `Term.destruct` hands it back as `Const` and it missed the datatype branch entirely: `[0, Nil]`. It now takes the same path as an applied constructor, `{"constructor" : "Nil", "args" : []}`. - **An empty array, set or map** stopped the JSON writer part way through the document. `Model.dimension_of_map` takes the dimensions from an index of the map, and an empty one has none to take, so `MIL.choose` raised `Not_found` into an `assert false` in the middle of a stream. The sizes of an empty map are now reported as zeroes. A dimension the type does not bound — the index of a set or a map — used to reach a second `assert false` on the fallback path, and is now reported as `null`, which the schema already allowed for. - **The list of subnodes** took its separator from whether the list had more entries, but a node standing for a global constant, a type ascription or a clocked expression prints nothing at all. A counterexample whose last subnodes were of that kind ended in a trailing comma. The separator now looks past the entries that print nothing. ### The schema `expr` and the `{"constructor", "args"}` value shape are documented in `schemas/kind2-output.json`. Both were already being emitted. ## Tests The regression suite reads exit codes alone, so nothing in it noticed any of this. `tests/test_output_formats.py` runs six models covering each shape above through both formats and checks that the output parses, and that property names holding quotes, backslashes and angle brackets survive a round trip unchanged rather than being rewritten. Ten of its fifteen cases fail without the changes in this PR. Two models are added for it: one with a property expression that spans several lines (the reproducer from #1467) and one whose properties are named with the characters the two formats give a meaning to. Both are `success` cases, so the rest of the suite runs them too. `tests/ounit/utils/testLib.ml` covers the two escapers directly. ## Downstream consumers Checked against `kind2-java-api`, `kind2-language-server` and `vscode-kind2` by building the API from source and reading the output of every model in the regression tree (639) through `Result.analyzeJsonResult`, with Kind 2 binaries built from this branch and from its merge base. Neither the language server nor the vscode extension parses Kind 2 output itself: the server drives the Java API, and everything it forwards to the extension has been re-serialized by gson, so the extension's strict `JSON.parse` only ever sees well-formed JSON. Neither uses the XML format at all. So the Java API is the only thing between Kind 2 and either of them. **One change needs the API updated first**, which kind2-mc/kind2-java-api#25 does. Writing a constructor that takes no fields as `{"constructor": "Nil", "args": []}` is correct, but gson parses leniently and had been reading the old bare `Nil` as the string `"Nil"`. `Type.getType` has no case for `"datatype"`, so such a stream is treated as an enumeration and its value read with `getAsString()`, which throws on an object. Seven models in the tree regress without that API change; with it, both output shapes read identically. Two things this PR fixes for them, which they hit today: - A `file` field holding a Windows path (`C:\models\top.lus`) is not just invalid JSON, it is invalid in a way gson rejects rather than tolerates: `\m` is not an escape. The whole `Result` throws `JsonSyntaxException`, so on Windows any diagnostic carrying a path would have taken the run down with it. - The counterexample this PR stops truncating (`gen_call_in_type_decl.lus`, the empty set) threw `JsonSyntaxException` in the API. Worth recording about #1467 itself: gson accepts raw newlines inside a string, so the reported bug never reached these three. It broke strict parsers, which is every other consumer, including the `json.load` in the issue. One pre-existing API bug turned up that is unrelated to output format and not addressed in either PR: Kind 2 reports a real produced by a division by zero as `{"num": 1, "den": 0}`, and `RealValue` divides by that denominator, so `test-div-by-zero.lus` throws `ArithmeticException: / by zero`. ## Not in this PR The JSON output still does not validate against the shipped schema, for reasons that predate this work and need a call on whether the schema or the output is the thing to change: - `isCandidate` is declared `boolean` but emitted as the string `"false"` - the `kind2Type` enum has no `adt`, and spells the machine integer types `int8`/`uint8` where the output writes `sint<8>`/`uint<8>` - the stream `class` enum has no `constant` or `ghost` Happy to take these on separately. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

Follow-up to #1549. That PR made the machine-readable output parseable; this one makes the JSON say what `schemas/kind2-output.json` says it says. The schema is what a consumer writes its reader against, and the two had drifted apart in five places. Nothing was looking: the regression suite reads exit codes, and the checks added with #1549 ask only whether the output parses. Validating every model in the tree against the schema finds **2152 violations of 5 kinds across 639 models**. ## What changes One is the output's fault. Four are gaps in the schema, which had not kept up with what Kind 2 prints. | | violations | where the fault is | |---|---|---| | `isCandidate` written as `"false"`, a string | 1864 | output — the schema and the XML both call it a boolean | | `source: "Termination"` | 116 | schema — the source arrived with recursive functions | | `type: "adt"` | 102 | schema | | `class: "constant"`, `class: "ghost"` | 58 | schema | | `type: "uint<8>"`, `"sint<8>"` … | 12 | schema — see below | `isCandidate` is now written as `%b`. The XSD already types it `xs:boolean` and `"false"` is a valid `xs:boolean` lexical form, so the XML was already conformant and is untouched. The `kind2Type` machine integers need more than a new enum entry. Kind 2 has two surface syntaxes for them — the fixed `uint8`…`uint64` keywords, and `uint<N>`/`sint<N>` for [any concrete size](https://kind.cs.uiowa.edu/kind2_user_doc/2_input/3_machine_ints.html) — and the JSON output names every one of them in the general form. The schema listed only the eight fixed names, which cannot express a width like `uint<24>` at all. `kind2Type` is now an `anyOf` of the names and a pattern for the general form. The eight fixed names are kept: the JSON output does not produce them, but making the schema stricter would reject documents it used to accept, for no gain. ## Tests `tests/test_output_schema.py` runs every model in the regression tree and validates its output against the schema. It is one test that fans out over eight threads, and takes about 14s. Reverting both the schema and the output change makes it fail with the five kinds above, commonest first: ``` 2152 schema violations over 639 models, of 17 kinds, commonest first: 1864 isCandidate: 'false' is not of type 'boolean' 116 source: 'Termination' is not one of ['Assumption', 'Guarantee', ...] 73 counterExample/streams/type: 'adt' is not one of [...] 33 counterExample/streams/class: 'constant' is not one of ['input', 'output', 'local'] 24 counterExample/subnodes/streams/type: 'adt' is not one of [...] ``` Validating against the `results` union directly reports why each object did not match every *other* member of it too, which buries the one failure that matters, so each object is checked against the definition its `objectType` names. Array indices come out of the path before the kinds are counted, or a single gap reads as thousands of distinct ones. The check needs `jsonschema`, which `tests/run` now asks `uvx` for. A checkout without `uv` still runs: the test skips itself when the package is missing, the way the IC3IA tests skip when MathSAT is. ## Compatibility `isCandidate` is the only change a consumer can see. gson reads a JSON boolean and the string `"false"` the same way through `getAsBoolean()`, so `kind2-java-api` — and so the language server and the vscode extension — are unaffected. Checked by reading the output of all 639 models through `Result.analyzeJsonResult`, with kind2-mc/kind2-java-api#25 applied: one model fails, `test-div-by-zero.lus`, for the unrelated reason recorded in that PR. ## Not in this PR The XML output has its own gaps against `kind2-output.xsd`, and one of them is a crash rather than a mismatch. They want their own change, and it is larger than this one: - **An arbitrary-width machine integer takes the XML writer down.** `pp_print_type` in `lustrePath.ml` matches the four widths it knows and raises `Invalid_argument "pp_print_type: BV size not allowed"` on anything else, part way through writing a stream, truncating the document — the same failure shape as the empty set in #1549. A node taking a `uint<24>` input is enough. The JSON handles it. - **The two formats name machine integers differently**: `uint8` and `int8` in XML against `uint<8>` and `sint<8>` in JSON, for the same model. The `case "int8":` arms in `kind2-java-api`'s `Type.getType` are dead code because of it, so a machine integer arrives there as an `Enum` rather than an `Int`. Worth settling on one vocabulary. - The XSD is missing the `Termination` property source and the `constant` stream class, as the JSON schema was, and a `<Log>` element carries a `file` attribute that `GenericLogType` does not declare. - `Results` requires `Property`, `AnalysisStart` and `AnalysisStop` at least once each, so no run that stops at a parse error can validate. That is a structural change to the content model, not a widening. Happy to take these on next. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

Closes kind2-mc#1467. `--json` output is not parseable when a property expression pretty-prints across more than one line: the `"expr"` field embeds the raw newlines. The field was written into the document with no escaping at all, and the helper that should have done it would not have been enough on its own — so this PR fixes the escaping in both machine-readable formats, and the ways the trace printers had of writing something neither format could read back. Checking the fix over the regression tree turned up eleven more models whose JSON no consumer could parse and twenty-three whose XML was not well-formed. All of them are fixed here. Every model in the tree now produces parseable JSON and well-formed XML. ## What changes ### The escapers `escape_json_string` escaped none of what it claimed to. `Str.global_replace` reads `\\` in a replacement template as one literal backslash, so the backslash rule was a no-op; quotes were rewritten to `'` rather than escaped, and tabs, carriage returns and the rest of the control range were passed through raw. It is now a single pass that escapes `"`, `\`, `\b`, `\f`, `\n`, `\r`, `\t` and `\u00xx`, leaving bytes at or above `0x80` alone so UTF-8 passes through as itself. `escape_xml_string` did not escape quotes, so a property named with one ended its attribute early. It also substituted `&` last, so the ampersands its own `<` and `>` introduced were escaped again: a `<` in a log message came out as `&lt;`. It is now a single pass as well. | | Before | After | |---|---|---| | `C:\models\top.lus` in JSON | `C:\models\top.lus` (decodes back with a tab and a newline) | `C:\\models\\top.lus` | | `a "quoted" name` in JSON | `a 'quoted' name` | `a \"quoted\" name` | | a tab in a log message | raw, not legal in a JSON string | `\t` | | `a "quoted" name` in XML | `name="a "quoted" name"` | `name="a "quoted" name"` | | `<` in a log message | `&lt;` | `<` | Every name, file path and scope written into either format now goes through the escaper for that format. That covers the `name`, `top`, `concrete` and `abstract` attributes, which used to take the name of a monomorphized node raw — and that name carries its type arguments in angle brackets, so `<AnalysisStart concrete="O<int>,N<int>">` was not well-formed. ### Values and types in a trace - **A stream of an uninterpreted sort** reported its type as the bare sort name. In XML that made the name an attribute of its own with no value: `<Stream name="init" COUNTER class="input">`. In JSON it was an unquoted `"name" : COUNTER`. Both schemas already describe the right shape (`abstrName`, and a `typeInfo.name` string), and the printers now match it. - **A value of an uninterpreted sort** (`COUNTER.0`) was written bare. Any value JSON has no literal of its own for is now written as a string. - **A constructor that takes no fields** is a constant rather than an application, so `Term.destruct` hands it back as `Const` and it missed the datatype branch entirely: `[0, Nil]`. It now takes the same path as an applied constructor, `{"constructor" : "Nil", "args" : []}`. - **An empty array, set or map** stopped the JSON writer part way through the document. `Model.dimension_of_map` takes the dimensions from an index of the map, and an empty one has none to take, so `MIL.choose` raised `Not_found` into an `assert false` in the middle of a stream. The sizes of an empty map are now reported as zeroes. A dimension the type does not bound — the index of a set or a map — used to reach a second `assert false` on the fallback path, and is now reported as `null`, which the schema already allowed for. - **The list of subnodes** took its separator from whether the list had more entries, but a node standing for a global constant, a type ascription or a clocked expression prints nothing at all. A counterexample whose last subnodes were of that kind ended in a trailing comma. The separator now looks past the entries that print nothing. ### The schema `expr` and the `{"constructor", "args"}` value shape are documented in `schemas/kind2-output.json`. Both were already being emitted. ## Tests The regression suite reads exit codes alone, so nothing in it noticed any of this. `tests/test_output_formats.py` runs six models covering each shape above through both formats and checks that the output parses, and that property names holding quotes, backslashes and angle brackets survive a round trip unchanged rather than being rewritten. Ten of its fifteen cases fail without the changes in this PR. Two models are added for it: one with a property expression that spans several lines (the reproducer from kind2-mc#1467) and one whose properties are named with the characters the two formats give a meaning to. Both are `success` cases, so the rest of the suite runs them too. `tests/ounit/utils/testLib.ml` covers the two escapers directly. ## Downstream consumers Checked against `kind2-java-api`, `kind2-language-server` and `vscode-kind2` by building the API from source and reading the output of every model in the regression tree (639) through `Result.analyzeJsonResult`, with Kind 2 binaries built from this branch and from its merge base. Neither the language server nor the vscode extension parses Kind 2 output itself: the server drives the Java API, and everything it forwards to the extension has been re-serialized by gson, so the extension's strict `JSON.parse` only ever sees well-formed JSON. Neither uses the XML format at all. So the Java API is the only thing between Kind 2 and either of them. **One change needs the API updated first**, which kind2-mc/kind2-java-api#25 does. Writing a constructor that takes no fields as `{"constructor": "Nil", "args": []}` is correct, but gson parses leniently and had been reading the old bare `Nil` as the string `"Nil"`. `Type.getType` has no case for `"datatype"`, so such a stream is treated as an enumeration and its value read with `getAsString()`, which throws on an object. Seven models in the tree regress without that API change; with it, both output shapes read identically. Two things this PR fixes for them, which they hit today: - A `file` field holding a Windows path (`C:\models\top.lus`) is not just invalid JSON, it is invalid in a way gson rejects rather than tolerates: `\m` is not an escape. The whole `Result` throws `JsonSyntaxException`, so on Windows any diagnostic carrying a path would have taken the run down with it. - The counterexample this PR stops truncating (`gen_call_in_type_decl.lus`, the empty set) threw `JsonSyntaxException` in the API. Worth recording about kind2-mc#1467 itself: gson accepts raw newlines inside a string, so the reported bug never reached these three. It broke strict parsers, which is every other consumer, including the `json.load` in the issue. One pre-existing API bug turned up that is unrelated to output format and not addressed in either PR: Kind 2 reports a real produced by a division by zero as `{"num": 1, "den": 0}`, and `RealValue` divides by that denominator, so `test-div-by-zero.lus` throws `ArithmeticException: / by zero`. ## Not in this PR The JSON output still does not validate against the shipped schema, for reasons that predate this work and need a call on whether the schema or the output is the thing to change: - `isCandidate` is declared `boolean` but emitted as the string `"false"` - the `kind2Type` enum has no `adt`, and spells the machine integer types `int8`/`uint8` where the output writes `sint<8>`/`uint<8>` - the stream `class` enum has no `constant` or `ghost` Happy to take these on separately. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

Follow-up to kind2-mc#1549. That PR made the machine-readable output parseable; this one makes the JSON say what `schemas/kind2-output.json` says it says. The schema is what a consumer writes its reader against, and the two had drifted apart in five places. Nothing was looking: the regression suite reads exit codes, and the checks added with kind2-mc#1549 ask only whether the output parses. Validating every model in the tree against the schema finds **2152 violations of 5 kinds across 639 models**. ## What changes One is the output's fault. Four are gaps in the schema, which had not kept up with what Kind 2 prints. | | violations | where the fault is | |---|---|---| | `isCandidate` written as `"false"`, a string | 1864 | output — the schema and the XML both call it a boolean | | `source: "Termination"` | 116 | schema — the source arrived with recursive functions | | `type: "adt"` | 102 | schema | | `class: "constant"`, `class: "ghost"` | 58 | schema | | `type: "uint<8>"`, `"sint<8>"` … | 12 | schema — see below | `isCandidate` is now written as `%b`. The XSD already types it `xs:boolean` and `"false"` is a valid `xs:boolean` lexical form, so the XML was already conformant and is untouched. The `kind2Type` machine integers need more than a new enum entry. Kind 2 has two surface syntaxes for them — the fixed `uint8`…`uint64` keywords, and `uint<N>`/`sint<N>` for [any concrete size](https://kind.cs.uiowa.edu/kind2_user_doc/2_input/3_machine_ints.html) — and the JSON output names every one of them in the general form. The schema listed only the eight fixed names, which cannot express a width like `uint<24>` at all. `kind2Type` is now an `anyOf` of the names and a pattern for the general form. The eight fixed names are kept: the JSON output does not produce them, but making the schema stricter would reject documents it used to accept, for no gain. ## Tests `tests/test_output_schema.py` runs every model in the regression tree and validates its output against the schema. It is one test that fans out over eight threads, and takes about 14s. Reverting both the schema and the output change makes it fail with the five kinds above, commonest first: ``` 2152 schema violations over 639 models, of 17 kinds, commonest first: 1864 isCandidate: 'false' is not of type 'boolean' 116 source: 'Termination' is not one of ['Assumption', 'Guarantee', ...] 73 counterExample/streams/type: 'adt' is not one of [...] 33 counterExample/streams/class: 'constant' is not one of ['input', 'output', 'local'] 24 counterExample/subnodes/streams/type: 'adt' is not one of [...] ``` Validating against the `results` union directly reports why each object did not match every *other* member of it too, which buries the one failure that matters, so each object is checked against the definition its `objectType` names. Array indices come out of the path before the kinds are counted, or a single gap reads as thousands of distinct ones. The check needs `jsonschema`, which `tests/run` now asks `uvx` for. A checkout without `uv` still runs: the test skips itself when the package is missing, the way the IC3IA tests skip when MathSAT is. ## Compatibility `isCandidate` is the only change a consumer can see. gson reads a JSON boolean and the string `"false"` the same way through `getAsBoolean()`, so `kind2-java-api` — and so the language server and the vscode extension — are unaffected. Checked by reading the output of all 639 models through `Result.analyzeJsonResult`, with kind2-mc/kind2-java-api#25 applied: one model fails, `test-div-by-zero.lus`, for the unrelated reason recorded in that PR. ## Not in this PR The XML output has its own gaps against `kind2-output.xsd`, and one of them is a crash rather than a mismatch. They want their own change, and it is larger than this one: - **An arbitrary-width machine integer takes the XML writer down.** `pp_print_type` in `lustrePath.ml` matches the four widths it knows and raises `Invalid_argument "pp_print_type: BV size not allowed"` on anything else, part way through writing a stream, truncating the document — the same failure shape as the empty set in kind2-mc#1549. A node taking a `uint<24>` input is enough. The JSON handles it. - **The two formats name machine integers differently**: `uint8` and `int8` in XML against `uint<8>` and `sint<8>` in JSON, for the same model. The `case "int8":` arms in `kind2-java-api`'s `Type.getType` are dead code because of it, so a machine integer arrives there as an `Enum` rather than an `Int`. Worth settling on one vocabulary. - The XSD is missing the `Termination` property source and the `constant` stream class, as the JSON schema was, and a `<Log>` element carries a `file` attribute that `GenericLogType` does not declare. - `Results` requires `Property`, `AnalysisStart` and `AnalysisStop` at least once each, so no run that stops at a parse error can validate. That is a structural change to the content model, not a widening. Happy to take these on next. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

daniel-larraz mentioned this pull request Sep 22, 2026

Make the JSON and XML output parseable kind2-mc/kind2#1549

Merged

daniel-larraz merged commit e9d2185 into kind2-mc:main Sep 22, 2026
1 check passed

daniel-larraz mentioned this pull request Sep 22, 2026

Make the JSON output match its schema kind2-mc/kind2#1550

Merged

This was referenced Sep 22, 2026

Read a machine integer as an integer #26

Merged

Read an infinite or undefined real #27

Merged

Navigation Menu

Repository navigation

Read algebraic datatype values - #25

Read algebraic datatype values#25
daniel-larraz merged 1 commit into
kind2-mc:mainfrom
daniel-larraz:read-algebraic-datatype-values

daniel-larraz commented Sep 22, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

daniel-larraz commented Sep 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What changes

Compatibility

Tests

Follow-ups, not in this PR

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

daniel-larraz commented Sep 22, 2026 •

edited

Loading