apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
427 stars 40 forks source link

Improve default ITF formatting #2257

Open shonfeder opened 1 year ago

shonfeder commented 1 year ago

The current formatting for ITF traces makes them hard for a human to read, simply due to unnecessary line breaks and indentation. E.g., here's an example of two states from a trace in the current formatting

    {
      "#meta": {
        "index": 0
      },
      "Names": {
        "#set": [
          "bar",
          "baz",
          "foo"
        ]
      },
      "paths": {
        "#set": [
          [
            {
              "tag": "Dir",
              "value": "."
            }
          ]
        ]
      }
    },
    {
      "#meta": {
        "index": 1
      },
      "Names": {
        "#set": [
          "bar",
          "baz",
          "foo"
        ]
      },
      "paths": {
        "#set": [
          [
            {
              "tag": "Dir",
              "value": "."
            },
            {
              "tag": "Dir",
              "value": "foo"
            }
          ],
          [
            {
              "tag": "Dir",
              "value": "."
            }
          ]
        ]
      }
    },

And here's the same trace formatted by Emac's json-mode:

    {
      "#meta": { "index": 0 },
      "Names": { "#set": ["bar", "baz", "foo"] },
      "paths": { "#set": [[{ "tag": "Dir", "value": "." }]] }
    },
    {
      "#meta": { "index": 1 },
      "Names": { "#set": ["bar", "baz", "foo"] },
      "paths": {
        "#set": [
          [
            { "tag": "Dir", "value": "." },
            { "tag": "Dir", "value": "foo" }
          ],
          [{ "tag": "Dir", "value": "." }]
        ]
      }
    },
thpani commented 11 months ago

I assume this is limited by ujson formatting? Perhaps we can just rely on people using external tools to format their JSON?