# 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.
- **State adoption in interactive simulation** — feeding a `(state …)` line
  at the start of a `--repl` session (typed, or as an event op in the JSON
  protocol) makes the simulator take over that state and simulate from
  there, exactly as a batch trace opening with a state assertion does. An
  unknown/unreachable state, a mid-run feed, or an unsupported model shape
  is refused without ending the session.
- `nucleos simulate --flush` (`-f`) includes the `<flush>` queue-drain event
  in interactive trails, matching `dzn traces --flush`. Off by default, so a
  drain renders silently unless the model's traces were cut in flush mode.
- `--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 that explodes into too many
  states now fails with a located error
  (`<file>:<line>:<col>: error: state explosion in handler …`, exit 1)
  instead of aborting. The limit is high enough that models in the
  2^16-outcomes range verify normally.

### Changed

- `nucleos verify` and `nucleos lts` are **faster on large models** — the
  state-space exploration is allocation-heavy, and both a faster allocator and
  fewer per-state allocations cut wall-clock by ~25% on the biggest components
  (output is byte-identical).
- Reading a shared interface variable (`port.var`) through an **`injected`**
  requires port is now rejected, as it already was for `external` ports — the
  provider's live state is not reachable across such a binding. (`dzn` only
  rejects the `external` case.)
- `nucleos simulate` produces the **same output on every surface** — batch
  text, `--output json`, `--repl`, and `--check-trace` all render a given
  trace identically. Verdicts (deadlock, livelock, illegal, non-compliance,
  invariant, range/queue errors) are deduced from the model itself rather
  than trusting markers in the input trace, and multi-leaf systems render
  with their 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 output is **byte-identical regardless of `--threads`** — including the
  single-worker default — and external-queue models are parallelised too.

### Fixed

- Interactive simulation surfaces an **injected requires notification the
  interface cannot produce** (e.g. feeding `timer.timeout` while the timer
  is idle) as a located `<illegal>` at the component behavior, delivered
  through the queue like any notification and carried on the `--repl` JSON
  turn envelope. Previously the event was silently swallowed — the session
  acknowledged it and the IDE sequence diagram showed nothing.
- Interactive simulation renders **per-emit state values** through a
  multi-event spontaneous group with interleaved assignments
  (`on inevitable: { s=C; world; s=B; world; s=A; }`): each queued
  out-event's `(state …)` line shows the value at that emission (C, then
  B), committing at the flush — matching dzn's interactive display. Such
  turns previously ended the session early. Quitting a
  `--repl --output json` session now also surfaces a verdict that only the
  final batch render of the session's trace deduces (e.g. a strict
  non-compliance on such a group), instead of reporting a clean `done`.
- 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.
- `simulate --repl` sessions **match batch exactly**: menu-driven sessions
  across defers, multiple provides ports, and shared state reconstruct the
  same trace a batch run produces, instead of collapsing or fabricating a
  non-compliance. An incurred verdict (`<illegal>`, `<queue-full>`, …) now
  locks the session (empty menu, further events rejected), so a run can no
  longer be driven past its verdict. Each `--repl --output json` envelope
  carries a top-level `"trail"` field a client can reconstruct against.
- LTS output is fully **deterministic**: reproducible run-to-run, across
  thread counts, and under machine load.
- Numerous `simulate` / `verify` fidelity fixes to match Dezyne semantics
  (system composition, defer, livelock, interface non-determinism, reply
  handling).
- Closed multiple well-formedness (WFC) gaps.
- `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.
