Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Revise the ITF format #2733

Merged
merged 3 commits into from
Sep 14, 2023
Merged

Revise the ITF format #2733

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d10eae5
simply the ITF format by using #bigint only
konnov Sep 14, 2023
59fe194
add the changelog entry
konnov Sep 14, 2023
848d3f4
add one empty line as per make fmt-fix
konnov Sep 14, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .unreleased/features/2732.md
View file
Open in desktop
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`
29 changes: 19 additions & 10 deletions docs/src/adr/015adr-trace.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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**

Expand All @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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",
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand Down
6 changes: 5 additions & 1 deletion tla-io/src/main/scala/at/forsyte/apalache/io/itf/ItfToTla.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
17 changes: 1 addition & 16 deletions tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

/**
Expand All @@ -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
*
Expand Down Expand Up @@ -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)
Expand Down
26 changes: 13 additions & 13 deletions tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 =>
Expand All @@ -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("")}",
Expand All @@ -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",
Expand All @@ -94,7 +94,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite {
| "#meta": {
| "index": 0
| },
| "N": 4
| "N": { "#bigint": "4" }
| }
| ]
|}""".stripMargin
Expand Down Expand Up @@ -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
Expand Down
Loading