From d10eae52917319ef6110629d239d226e7d4eb771 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 14 Sep 2023 11:12:45 +0200 Subject: [PATCH 1/3] simply the ITF format by using #bigint only --- docs/src/adr/015adr-trace.md | 29 ++++++++++++------- .../at/forsyte/apalache/io/itf/ItfToTla.scala | 6 +++- .../io/lir/ItfCounterexampleWriter.scala | 18 +----------- .../io/lir/TestItfCounterexampleWriter.scala | 26 ++++++++--------- 4 files changed, 38 insertions(+), 41 deletions(-) diff --git a/docs/src/adr/015adr-trace.md b/docs/src/adr/015adr-trace.md index d81fe0149f..a8831f65bf 100644 --- a/docs/src/adr/015adr-trace.md +++ b/docs/src/adr/015adr-trace.md @@ -1,8 +1,8 @@ # ADR-015: Informal Trace Format in JSON -| authors | proposed by | last revised | -| -------------------------------------- | ---------------------------- | --------------: | -| Igor Konnov | Vitor Enes, Andrey Kupriyanov | 2022-11-03 | +| authors | proposed by | last revised | +| -------------------------------------- | ---------------------------- |-------------:| +| Igor Konnov | Vitor Enes, Andrey Kupriyanov | 2023-09-14 | **Table of Contents** @@ -22,6 +22,12 @@ communicate counterexamples to engineers who are not familiar with TLA+. This ADR-015 contains a very simple format that does not require any knowledge of TLA+ and can be easily integrated into other tools. +## Revisions + +**Rev. 2023-09-14.** Each integer value `num` is now represented as `{ #bigint: "num" }`. +The use of JSON numbers is not allowed anymore. This simplifies custom parsers for ITF, +see [Consequences](#consequences). + ## Context A TLA+ execution (called a behavior in TLA+) is a very powerful concept. It can @@ -276,11 +282,8 @@ specified in the field `vars`. Each state must define a value for every specifie 1. A JSON string literal, e.g., `"hello"`. TLA+ strings are written as strings in this format. -1. 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. - 1. 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* + impose limits on integer values, see [RFC7159][]. Big and small integers *must be* written in this format. 1. A list of the form `[ , ..., ]`. A list is just a JSON array. TLA+ sequences are written as lists in this format. @@ -325,7 +328,7 @@ For example: The counterexample to `NoSolution` may be written in the ITF format as follows: -```js +```json { "#meta": { "source": "MC_MissionariesAndCannibalsTyped.tla", @@ -420,7 +423,7 @@ proposed format in the [PR comments](https://github.com/informalsystems/apalache/pull/1190). In a regular approach we would treat all expressions uniformly. For example: -```js +```json // proposed form: "hello" // regular form: @@ -455,7 +458,13 @@ we should keep it in mind and use schemas, when the need arises. Did it work, not work, was changed, upgraded, etc. --> -Reserved for the future. +We have found that the ITF format is easy to produce and relatively easy to parse. + +**Ambiguity in the representation of integers**. As it was brought up in the initial +discussions, the choice between representing integers +as JSON numbers, e.g., `123` and objects, e.g., `{ #bigint: "123" }`, makes it harder to +write a parser of custom ITF traces. Hence, we have decided to keep only the object format, +as the more general of the two representations. [ADR005]: https://apalache.informal.systems/docs/adr/005adr-json.html diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/itf/ItfToTla.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/itf/ItfToTla.scala index 529dae5c4d..9231b0ce78 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/itf/ItfToTla.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/itf/ItfToTla.scala @@ -143,7 +143,11 @@ class ItfToTla[T <: JsonRepresentation]( asStr(json.getFieldOpt(BIG_INT_FIELD).get).map { bi => tla.int(BigInt(bi)) } - } else asInt(json).map { i => tla.int(BigInt(i)) } + } else { + // We keep this case for the backwards compatibility with the older versions of ITF. + // Apalache itself does not produce this case any longer. + asInt(json).map { i => tla.int(BigInt(i)) } + } case SeqT1(elemT) => for { diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala index 3f1039fa27..f948ddc64a 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala @@ -8,7 +8,6 @@ import at.forsyte.apalache.tla.lir.values.{TlaBool, TlaInt, TlaStr} import java.io.PrintWriter import java.util.Calendar -import scala.collection.immutable.Map import scala.collection.mutable /** @@ -26,17 +25,6 @@ class ItfCounterexampleWriter(writer: PrintWriter) extends CounterexampleWriter } object ItfCounterexampleWriter { - - /** - * The minimal value that can be reliably represented with Double in JavaScript. - */ - val MIN_JS_INT: BigInt = -BigInt(2).pow(53) + 1 - - /** - * The maximal value that can be reliably represented with Double in JavaScript. - */ - val MAX_JS_INT: BigInt = BigInt(2).pow(53) - 1 - /** * Produce a JSON representation of a counterexample in the ITF format * @@ -108,11 +96,7 @@ object ItfCounterexampleWriter { private def exToJson: TlaEx => ujson.Value = { case ValEx(TlaInt(num)) => - if (num >= MIN_JS_INT && num <= MAX_JS_INT) { - ujson.Num(num.toDouble) - } else { - ujson.Obj(BIG_INT_FIELD -> ujson.Str(num.toString(10))) - } + ujson.Obj(BIG_INT_FIELD -> ujson.Str(num.toString(10))) case ValEx(TlaBool(b)) => ujson.Bool(b) diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala index 50cb175f47..de50228e00 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala +++ b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala @@ -44,7 +44,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite { } /** - * Asserts that P(seq)(json1,json2) holds for every seq in nesetedAccess, where P(seq)(json1,json2) is defined as + * Asserts that P(seq)(json1,json2) holds for every seq in nestedAccess, where P(seq)(json1,json2) is defined as * - json1 = json2, if seq is empty, and * - if seq = h +: t, a conjunction of: * - json1 defines a field h, or list of length at least h @@ -54,7 +54,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite { * In other words, for every sequence Seq(s1,...,sn) in nestedFields json1.s1.s2.(...).sn and json2.s1.s2.(...).sn * must be well defined and equal. */ - def assertEqualOver(nesetedAccess: Seq[AbstractAccess]*)(json1: Value, json2: Value): Unit = { + def assertEqualOver(nestedAccess: Seq[AbstractAccess]*)(json1: Value, json2: Value): Unit = { def prop(seq: Seq[AbstractAccess])(v1: Value, v2: Value): Boolean = seq match { case Seq() => v1 == v2 case h +: t => @@ -65,7 +65,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite { } yield prop(t)(v1AtH, v2AtH) ).getOrElse(false) } - nesetedAccess.foreach { accessSeq => + nestedAccess.foreach { accessSeq => assert( prop(accessSeq)(json1, json2), s": Inputs differ on _${accessSeq.map(a => s"(${a.toString})").mkString("")}", @@ -81,7 +81,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite { List(("0", SortedMap("N" -> tla.int(4).build))), ) val rawExpected = - """{ + s"""{ | "#meta": { | "format": "ITF", | "format-description": "https://apalache.informal.systems/docs/adr/015adr-trace.html", @@ -94,7 +94,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite { | "#meta": { | "index": 0 | }, - | "N": 4 + | "N": { "#bigint": "4" } | } | ] |}""".stripMargin @@ -187,20 +187,20 @@ class TestItfCounterexampleWriter extends AnyFunSuite { | "states": [ | { | "#meta": { "index": 0 }, - | "a": 2, + | "a": { "#bigint": "2" }, | "b": "hello", - | "c": [ 3, { "#bigint": "1000000000000000000" } ], - | "d": { "#set": [ 5, 6 ] }, - | "e": { "foo": 3, "bar": true }, - | "f": { "#tup": [ 7, "myStr" ] }, - | "g": { "#map": [[1, "a"], [2, "b"], [3, "c"]] }, + | "c": [ { "#bigint": "3" }, { "#bigint": "1000000000000000000" } ], + | "d": { "#set": [ { "#bigint": "5" }, { "#bigint": "6" } ] }, + | "e": { "foo": { "#bigint": "3" }, "bar": true }, + | "f": { "#tup": [ { "#bigint": "7" }, "myStr" ] }, + | "g": { "#map": [[{ "#bigint": "1" }, "a"], [{ "#bigint": "2" }, "b"], [{ "#bigint": "3" }, "c"]] }, | "h": { "#map": [] }, - | "i": { "#map": [[1, "a"]] }, + | "i": { "#map": [[{ "#bigint": "1" }, "a"]] }, | "j": { "#unserializable": "[BOOLEAN → Int]" }, | "k": { "#unserializable": "SUBSET BOOLEAN" }, | "l": { "#unserializable": "Int" }, | "m": { "#unserializable": "Nat" }, - | "n": { "tag": "Baz", "value": { "foo": 3, "bar": true }} + | "n": { "tag": "Baz", "value": { "foo": { "#bigint": "3" }, "bar": true }} | } | ] |}""".stripMargin From 59fe1946e3fefc907a2bdeacf860bb1eb09e075f Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 14 Sep 2023 11:14:21 +0200 Subject: [PATCH 2/3] add the changelog entry --- .unreleased/features/2732.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/features/2732.md diff --git a/.unreleased/features/2732.md b/.unreleased/features/2732.md new file mode 100644 index 0000000000..5cd634822b --- /dev/null +++ b/.unreleased/features/2732.md @@ -0,0 +1 @@ +- Revise the ITF format: Use only `{ "#bigint": "num" }`, even for small integers` From 848d3f4535fca84908be7dd433c62f14bc01d5ff Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 14 Sep 2023 11:33:04 +0200 Subject: [PATCH 3/3] add one empty line as per make fmt-fix --- .../at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala | 1 + 1 file changed, 1 insertion(+) diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala index f948ddc64a..57b9fbf46c 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala @@ -25,6 +25,7 @@ class ItfCounterexampleWriter(writer: PrintWriter) extends CounterexampleWriter } object ItfCounterexampleWriter { + /** * Produce a JSON representation of a counterexample in the ITF format *