Merge pull request #2733 from informalsystems/igor/itf2732

Revise the ITF format
apalache-mc · Sep 14, 2023 · 5c0e659 · 5c0e659
2 parents 403eb14 + 848d3f4
commit 5c0e659
Show file tree

Hide file tree

Showing 5 changed files with 39 additions and 40 deletions.
diff --git a/.unreleased/features/2732.md b/.unreleased/features/2732.md
@@ -0,0 +1 @@
+- Revise the ITF format: Use only `{ "#bigint": "num" }`, even for small integers`
diff --git 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 `[ <expr>, ..., <expr> ]`. 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
@@ -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
@@ -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
 
 /**
@@ -27,16 +26,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 +97,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
@@ -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
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		- Revise the ITF format: Use only `{ "#bigint": "num" }`, even for small integers`