**A minor line, opened by Layer 1's predicate rule.** A Layer 1 `invariant`,
`action_property`, `precondition` or `postcondition` that returns a non-boolean is now
reported rather than counted as holding (#418). The model checker already refused the same
predicate. Code whose check returned a truthy non-boolean passed under 0.5.0 and is now
reported, which is why this is 0.6.0. To upgrade, change the requirement, then make any such
check return `true` or `false`. `ExTLA.ModelChecker.run/2` and `assert_spec/2` now honour a
constant's `default:`, as the Mix tasks always did (#417). ExTLA installs from Hex as
`{:extla, "~> 0.6.0"}`.
The rest is the documentation, made fit for a public reader and checked against the code:
- a short README;
- HexDocs that publish the DSL reference, the examples and a new reference page, and group
the modules by use;
- module docs that list `run/2`'s options and no longer narrate the project's history;
- a changelog written for users;
- guides whose output blocks are compared with what the tool really prints.
- **The repository's public home is GitHub, and everything that ships says so** (#402, for
#396). `mix.exs` declares `source_url` and `homepage_url`, so the docs' "View source"
links work and point at the release tag, and the package declares its links (GitHub,
Changelog). The version links at the end of this file point at GitHub.
- **The README is a short front door** (#403, for #395). It says what ExTLA does in one
line, then why it matters when an LLM writes your concurrent code, then installation, one
example, the task list and links to everything else. The package description and the
`ExTLA` module docs open with the same line. The TLC agreement tables and benchmarks that
filled half the old README now sit beside the corpus they measure, in
`test/differential/README.md`.
- **The docs publish only what a user needs** (#404, for #397). Of `spec/`, HexDocs now
carries the DSL reference and the examples, and both have lost their history paragraphs.
The rest of the specification is design material, linked on GitHub where a page needs it.
A new guide page, `guides/reference.md`, holds the user-facing facts that lived only in
the departing files: how `mix extla.check` and `ExTLA.ModelChecker.run/2` differ on
liveness, what state constraints, symmetry and `--workers` each cost and refuse, how to
read the coverage report, the JSON result schema, what conformance checks, Layer 1's
test helpers, telemetry and overhead, and what ExTLA is not. The `ExTLA` module docs and
this file now agree that the changelog is the record of what is built.
- **The API docs group modules by what you do with them** (#405, for #397): specifications,
model checking, Layer 1, Layer 3, and Internals last for the engine modules a user never
calls, such as `ExTLA.Invariant.Runtime`. `ExTLA` heads the list.
- **The module docs and usage rules say what the code does, and list the options** (#407, for
#399). `ExTLA.ModelChecker.run/2` and `ExTLA.Simulation.run/2` document every option with
its default; before, they were only in typespec comments. `usage-rules.md` no longer shows
a `--check-liveness` flag that does not exist. It now says the CLI skips liveness with a
warning under symmetry or `--workers`, while the API raises. It also names the right
diagnostic for assigning a variable twice, and covers `config :extla`, `use` ordering and
the optional `jason`. `assert_spec/2` says liveness is off unless asked for, and
`mix extla.check` documents per-spec `symmetry:`. `mix extla.simulate` says how its
server starts, and `mix extla.replay` describes its trace file correctly and lists
`--format`. Stale `TLA.` names and arities are fixed.
- **The module docs are about the library, not its history** (#408, for #399). About 40
modules carried how a behaviour was found and fixed: issue numbers, test paths, CI, the
differential corpus, mutation testing, decision-log numbers, and pointers into
specification files the docs no longer publish. Each is rewritten to say what the code
does and why. Where a doc pointed at an unpublished reason, it now states the reason or
links the reference guide.
- **The output shown in the guides is the output the tool prints** (#409, for #398). Every
block of `mix extla.*` output in getting-started and the tutorial is now compared with the
command's real output when the guides are tested. A block that shows only part of the
output says so, and its lines must still appear in order. Twenty-five blocks that had
drifted are regenerated. They were missing trace banners, used an old lasso rendering,
had a coverage count one off, and dropped transition counts. Page 10's DOT example now
comes from a spec shown on the page.
- **Getting started and the tutorial say what the tool does, and where each option applies**
(#410, for #398). The pages now say which options are for `ExTLA.ModelChecker.run/2` and
`assert_spec/2` only (`state_constraint:`, `check_deadlock:`, `check_liveness:`). They
say that `mix extla.check` checks liveness on its own, and where the CLI reads constants
and symmetry from. Wrong claims are corrected: an invariant's `desc:` is not printed in a
counterexample, `--strict-coverage` never fails on a live terminal, and
`mix extla.visualize` refuses with "more than N". The pages gain the optional `jason` and
`telemetry` dependencies, the sequence operations, `mix extla.replay`'s exit code 3 and
driving flags, the `:state_functions` limit of Layer 1, and
`ExTLA.PropertyTest.action_sequences/3`. Passages about how ExTLA itself is tested are
gone.
- **Install from Hex** (#424, for #423). The README and getting-started install ExTLA as
`{:extla, "~> X.Y.0"}`. Use the three-part requirement: before 1.0 a new minor version can
change the interface, and `~> X.Y` would take it.
- **This changelog is written for users** (#406, for #397). Entries for CI, test tooling and
other work only the repository sees are gone, and the remaining entries are shorter.
- **`ExTLA.ModelChecker.run/2` honours a constant's `default:`** (#417, for #415). A spec
that declares `constant :max, default: 3` checked under `mix extla.check` but raised from
`run/2`, `check_safety/2`, `explore/2` and `ExTLA.Spec.Test.assert_spec/2`: "the type of :n
refers to ^max, which this run did not assign". Declared defaults now fill in what
`constants:` leaves out, and an explicit constant still wins. Application config is still
read only by the Mix tasks.
- **`--verify-symmetry`'s report lists its differences in a fixed order** (#410). The
lines naming what differed with and without the reduction came out in an order that
could change from one run to the next. They now always read status, deadlock, refuted,
never enabled.
- **Layer 1 refuses a predicate that returns a non-boolean, as Layer 2 does** (#418, for
#401). An `invariant`, `action_property`, `precondition` or `postcondition` returning a
truthy non-boolean used to count as holding. A common way to get one is
`n >= 0 and status`, which evaluates to `status`. The model checker already refused the
same predicate. It is now reported through the configured mode, naming the value
("returned :ok, which is not a boolean"): `:enabled` raises `ExTLA.Invariant.Violation`
and `:log_only` logs it. **This can surface reports in code that passed before.** Add the
missing comparison so the predicate returns `true` or `false`.
32 commits since v0.5.0, merges included.
Tagged at 3e099b83778c.
