# nucleos Changelog Version `0.1.0-dev.8`. ## Added - **Trace source locations in `simulate --output json`** — activities in the P5 sequence-diagram trace now carry `location` (`file-name`/`line`/`column`), resolved from the executing statement and handler as the simulation runs: call arrows point at the trigger of the handler they actually enter (the executing guard block, not the first one in source order), return arrows at that handler's `on` keyword, out-calls at their call site — matching `dzn simulate -l` attribution byte-for-byte across the golden corpus. Enables click-to-source (`go_to`) navigation from the IDE sequence diagram. Text output is unchanged. - **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 `` 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 ` — rewrite a `.dzn` with every identifier replaced by `_` 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 (`::: 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. - `nucleos code` and `nucleos graph` — code generation and system-view / state-diagram graphs, delegated to the legacy `dzn` toolchain, which nucleos finds at `legacy/dzn` beside its own binary (or via `$NUC_DZN`). Arguments pass through untouched and `dzn`'s exit status is preserved, so anything that called `dzn code` or `dzn graph` keeps working through nucleos. `--help` forwards too. ## Changed - `--output` belongs to `verify` and `simulate`, not to every subcommand. `nucleos code --output DIR` now reaches `dzn` instead of being rejected as an invalid report format; the short and long spellings no longer disagree. - A cross-cutting flag aimed at a subcommand that ignores it now warns and carries on, naming the subcommands that do honour it. It will become an error in a later release. - Clearer command line — one line per option in subcommand help, a missing or mistyped subcommand is named with a suggestion instead of a wall of usage, and internal development subcommands no longer appear. - Windows: the legacy `dzn` is located as `dzn.cmd`, matching what the Dezyne distribution ships. - `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 Much of this came from users running nucleos against their own models. - Expression functions in guards are evaluated — such a call was read as `true` whatever its real value, so any result depending on that guard could be wrong: verdicts, traces, or the state space explored. Guards, invariants, replies and initialisation now evaluate them. - Nondeterministic arms nested in guarded compound blocks are resolved — the dominant style in real models. - Non-compliance verdicts for cross-port round-trips and refused provides emits, with compliance now decided locally in simulate. - `simulate --repl` no longer wedges when it receives an unexpected event at a quiescent point. - A pure-inevitable interface can be driven interactively. - Invalid models are reported with a located error instead of crashing or being accepted — expression functions at global scope, global block functions used as predicates, non-boolean constant guards, `reply()` with multiple values, and several inputs that previously panicked. - `` is a first-class member of the eligible/label set, matching `dzn`, and a closed livelock cycle is terminal — the trace truncates rather than bailing. - Deferred events, forks, choice suspension, empty traces and initial state, and external delivery under a full queue match `dzn` in many more cases. - `verify` and `lts` are faster on large models — the deadlock check no longer copies the graph, and leaf redirection uses an index instead of rescanning. - Interactive simulation drives a foreign component's injected requires port. A foreign child has no body to fire its requires injected port, so the port is stimulated from outside (`sut...`, as offered in the eligible set); the call now reaches the `<=> *` provider component and its reply returns to the same boundary, instead of the render stopping at an unbound port. - Interactive simulation surfaces an injected requires notification the interface cannot produce (e.g. feeding `timer.timeout` while the timer is idle) as a located `` 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 `` 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 (``, ``, …) 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 `` overflow that `verify` already reports — an unguarded spontaneous out-event on a requires external port floods the single-slot external queue. - `nucleos simulate` reports `` instead of `` 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.