mix extla.explore (ExTLA v0.6.0)

Explore a counterexample mix extla.check --format json already wrote, without running the checker again.

Usage

mix extla.explore Specs.DistributedLock --trace counterexample.json \
  --expr "waiting: length(state.waiting)" \
  --expr "quorum?: map_size(state.votes) * 2 > 3" \
  --changed-only

# from an earlier run or an incident, months later, with no checker in the loop
mix extla.check Specs.DistributedLock --format json > ce.json
mix extla.explore Specs.DistributedLock --trace ce.json --expr "len: length(state.log)"

--expr evaluates code you typed

An expression over a state is an anonymous function and there is no way to write one on a command line, so each --expr is compiled and evaluated — which is exactly what the Toolbox's Trace Explorer does with the expressions you type into it. This is a development task and the code it runs is the code you just wrote in your own shell; do not point it at a flag string from somewhere else.

Repeatable, one expression each. Inside one, the state is in scope two ways:

• each variable by its own name — --expr "length(waiting)";
• state, the whole map — --expr "length(state.waiting)", and the only way to reach a spec variable that is itself called state.

name: expression labels the row. Without a label the expression's own text is the label, so --expr "state.holder" is a row called state.holder. The label is recognised by parsing, not by splitting on a colon, so --expr "state.pc[:alice]" is one unlabelled expression rather than a row called state.pc[.

The file

--trace takes what mix extla.check --format json writes — the whole document, or a single trace object lifted out of it — and a lasso as readily as a trace.

The module argument is not decoration: ExTLA.Trace.from_json!/1 resolves the trace's atoms with String.to_existing_atom/1, so the spec has to be loaded before its counterexample can be decoded. A trace belonging to a different spec fails naming the atom that did not resolve, rather than quietly decoding into something else.

Exit codes

0  the table was rendered
1  a bad `--expr`, or a file that is not a counterexample for this spec