apalache-mc/apalache

Revise the ITF format

konnov opened this issue · 0 comments

konnov commented

The current version of ITF introduces two ways of serializing not-too-big integers:

  • A JSON integer, e.g., 123. According to RFC7159, JSON integers must be in the range: $[-2^{53}+1, 2^{53}-1]$. Integers in this range may be written as JSON integers.

  • A big integer of the following form: { "#bigint": "[-][0-9]+" }. We are using this format, as many JSON parsers impose limits on integer values, see RFC7159. Big and small integers may be written in this format.

Back then, I thought it was a good idea, but it introduces branching in every parser, which distinguishes between #bigint field and an integer field.

I was thinking of just keeping the #bigint field.