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

02-dsl-semantics.md §6 permits atoms, integers, binaries, tuples, lists, maps, MapSets 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.