The body of ExTLA.Trace.explore/3: named expressions evaluated at every state of a counterexample, rendered as a table.

A separate module for the reason ExTLA.StateGraph.Export is one — ExTLA.Trace is about regenerating a counterexample and checking it against the spec, and this is a rendering over the finished result. What the two share is deliberately small and lives on ExTLA.Trace as join/1, call/2, banner/1 and loop_note/2, so the table and format/1 cannot disagree about how a lasso flattens or how an action call is written.

The layout, and why it is not the obvious one

The obvious layout puts each step's binding in its column header. It does not survive contact with a real trace: begin_transfer(from: :alice, to: :bob, amount: 3) is 44 characters, and one such column consumes most of a terminal on its own. So the header carries the state number and the bare action name, and the bindings are listed under the table, where their length costs nothing:

═══ EXPLORE: mutual_exclusion ══════════════════════════════════

                  1        2        3        4        5
               init  request  request  acquire  release
  ──────────────────────────────────────────────────────
  waiting          0        1        2        1        1
  holder         nil      nil      nil   :alice      nil
  quorum?      false    false    false    false    false

  Bindings:
    2  request(client: :alice)
    3  request(client: :bob)
    4  acquire(client: :alice)
    5  release(client: :alice)
════════════════════════════════════════════════════════════════

Chunking is not a nicety

raft_election's counterexample — the trace the whole feature is for — is nineteen states. At eight characters a column that is 152 characters against the 68 format/1 rules to, so a renderer that emits one column per state cannot render its own motivating example. States are therefore chunked into groups that fit the budget, each group repeating the name column and labelled with the states it covers.

changed_only: true narrows a wide trace but cannot be relied on to: an expression that moves at every step is exactly the one worth watching, and it is never hidden.