# `ExTLA.State.Json`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/state/json.ex#L1)

The JSON form of a state term, and back again.

`02-dsl-semantics.md` §6 permits atoms, integers, binaries, tuples, lists, maps,
`MapSet`s and structs built from those. JSON has objects, arrays, strings and numbers,
so five of those eight have no JSON of their own and every one of them needs a tag — and
a binary that is not valid UTF-8 is not a JSON string either, so it gets one too (`"b64"`).

## Why this exists rather than `inspect/1`

`mix extla.check --format json` wrote states and bindings with `inspect/1`, which a person
can read and a machine cannot parse back. §05's own pipeline is
`mix extla.check --format json` into `mix extla.replay --trace counterexample.json`, and a
format that only goes one way cannot carry it. The human rendering is
`ExTLA.Trace.format/1` and stays exactly as it was.

    %{count: 1, status: :ready}
    #=> %{"m" => [[%{"a" => "count"}, 1], [%{"a" => "status"}, %{"a" => "ready"}]]}

Maps are pairs rather than JSON objects because a spec's map keys are usually atoms and
may be anything §6 permits — a JSON object would force every key to a string and lose
which ones were atoms.

## An atom the system does not already have is an error

A trace file is data from outside the program, and the atom table is never collected, so
a decoder that creates atoms from a file lets a large one exhaust it. Every atom a real
trace mentions exists already: the spec module that named it is loaded before its trace
is read.

One that does not raises `ArgumentError` — *"not an already existing atom"*, from
`String.to_existing_atom/1`. The usual cause is a trace belonging to a different
specification than the module it is being replayed against.

# `decode!`

The term a `encode/1` result came from.

Raises `ExTLA.State.Json.Error` on JSON this module did not write, and on an atom no
loaded module has ever mentioned.

# `encode`

A state term as data `Jason.encode!/1` accepts.

---

*Consult [api-reference.md](api-reference.md) for complete listing*