# Changelog

All notable changes to **nucleos** are documented in this file.

The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).

Pre-release versions follow the form `X.Y.Z-rc.N` (release candidates) or
`X.Y.Z-dev` (between-release development snapshots).

## [Unreleased]

### Added

- **Parallel LTS generation** — `--threads N` parallelises state-space
  exploration for `nucleos lts` and `nucleos verify`. A serial,
  order-preserving merge keeps the output identical for any thread count.
- **Interactive simulation** — `nucleos simulate --repl` steps a trace
  interactively; `--check-trace` validates a trace non-interactively.
- `--full-lts` (on `lts` / `verify`) forces a complete exploration, now that
  fail-fast is the default.
- `nucleos parse --list-models` and filename-free model selection.
- NDJSON streaming output for `nucleos verify`.
- Man pages and shell completions shipped in the release archives.
- `nucleos bug-report` — bundle diagnostic info (version + git SHA, host
  info, and optionally a flattened/anonymized model) into a single archive
  for attaching to a support ticket.
- `nucleos anonymize <FILE>` — rewrite a `.dzn` with every identifier
  replaced by `_<N>` and comments stripped, so a model can be shared
  without leaking source. Accepts stdin (`-`).
- `nucleos --version` embeds the git short SHA (e.g. `0.1.0-dev.4 (abc1234)`)
  so bug reports cite the exact build.
- **Nondeterministic external delivery** — multiple handlers for the same
  delivered external out-event (e.g. duplicate `on r.a()`) are explored as a
  nondeterministic fork; `verify` reports the component as non-deterministic
  with the shortest witness trace, matching dzn.
- **State-explosion diagnostics** — a handler whose exploration exceeds the
  internal budget (500 000 states) fails with a located, user-facing error
  (`<file>:<line>:<col>: error: state explosion in handler …`, exit 1)
  instead of an internal panic. The budget was raised 10× so models in the
  2^16-outcomes range verify normally.

### Changed

- `nucleos simulate` runs on a **new trace-rendering engine** across every
  surface — batch text, `--output json`, `--repl`, and `--check-trace` all
  produce the same output for the same trace. The engine deduces verdicts
  (deadlock, livelock, illegal, non-compliance, invariant, range/queue
  errors) from the model itself rather than trusting markers in the input
  trace, and renders multi-leaf systems with full internal-binding cascades.
- Simulate **diagnostics match `dzn simulate`'s detail**: verdicts come with
  located `component performs:` / `port expects:` lines, `no match; at …`
  context for unmatched inputs, forking-violation pairs, and
  `end of trail; stopping here:` info. `--output json` embeds the same
  detail in the trace `messages`, so IDE consumers see it too.
- Enum values in `(state …)` lines print in their shortest `Enum:Field`
  form everywhere (previously the declaring scope leaked in, e.g.
  `IContrast.EContrast:Sharper`); text and JSON output agree.
- `nucleos verify` and `nucleos lts` are **fail-fast by default**: they stop
  at the first error edge and report it. Pass `--full-lts` for the complete
  graph.
- `nucleos simulate` now runs the **well-formedness checker by default**
  (matching `verify`); opt out with `--skip-wfc`.
- LTS generation uses a **single parallel engine** at every thread count, so
  the `.aut` is byte-identical regardless of `--threads` — including the
  single-worker default — and external-queue models are parallelised too.

### Removed

- The hidden development subcommands `nucleos sim2`, `nucleos render`, and
  `nucleos replay` — all superseded by `nucleos simulate`, which now runs
  the same engine directly.

### Fixed

- Interactive simulation reaches **batch parity**: `--check-trace` and
  `--repl` render verdict rounds (including livelock unrolls and
  `<invariant>` merged into its closing step), eligible-action lists at
  verdicts, and end-of-trail handling exactly as a batch run of the same
  trace does.
- LTS output is fully **deterministic**: reproducible run-to-run, across
  thread counts, and under machine load (validated with injected scheduling
  jitter).
- `nucleos lts-diagnose` (dev) streams its per-state `[dbg]` exploration
  trace again — it had gone silent when LTS generation moved to the
  unified parallel engine (exploration-time state ids no longer matched
  the final numbering the `--state` target uses). The target is now
  resolved to its dispatching handler first, including targets reached
  through collapsed multi-edge prefix chains (spontaneous-requires /
  external delivery).
- Numerous `simulate` / `verify` fidelity fixes to match Dezyne semantics
  (system composition, defer, livelock, interface non-determinism, reply
  handling).
- Closed multiple well-formedness gaps surfaced by a differential fuzzer.
- `nucleos simulate` renders **multi-out spontaneous requires groups**
  (e.g. `on inevitable: { a; b; … }`) that previously could not be
  rendered.
- `nucleos simulate` (and `--check-trace`) now surface the external-queue
  `<queue-full>` overflow that `verify` already reports — an unguarded
  spontaneous out-event on a `requires external` port floods the
  single-slot external queue.
- `nucleos simulate` reports `<deadlock>` instead of `<non-deterministic>`
  when two conflicting handlers both settle at a stuck state, matching
  `dzn simulate`'s per-boundary precedence.
- Interface non-determinism that was hidden behind a nested block-local
  shadowing a state variable is now detected (the block-local no longer
  leaks past its scope), matching `dzn verify`.
- `nucleos` no longer rejects a legal interface that declares an `enum`
  (or subint) of the same name at the interface top level **and** inside
  `behavior`: the inner declaration shadows the outer (matching dzn's
  frontend) and its members resolve correctly.

## [0.1.0] - 2026-05-09

- Initial baseline: parser, well-formedness checker, simulator,
  verifier, LTS generator with cursor + DAG + step_frontier engines.
