# Dezyne Simulator

A Rust implementation of a Dezyne model simulator, verifier, and LTS (Labelled
Transition System) generator. Parses Dezyne `.dzn` models and can:

- **Parse / well-formedness check** (`nucleos parse`)
- **Simulate** a trace — batch replay, or interactively (`nucleos simulate`)
- **Verify** determinism / illegal / deadlock properties (`nucleos verify`)
- **Generate LTS** in `.aut` format for formal verification (`nucleos lts`)

## Build

```bash
cargo build --release
```

The binary lands at `./target/release/nucleos`. Scripts take that path from
`$SIM` in `config.sh` — set `SIM=/path/to/nucleos` to override. (A few scripts
under `scripts/` use their own `NUCLEOS_BIN` / `DZN_BIN` instead; their headers
say so.)

`nucleos --version` reports the Cargo.toml version + git short SHA, e.g.
`nucleos 0.2.0-dev (6c5cf44)` — see [`RELEASING.md`](./RELEASING.md) for how
the dev / rc / official release flow works.

### Local macOS package (Apple Silicon)

[`scripts/package-macos.sh`](./scripts/package-macos.sh) builds natively and
bundles a **relocatable** mCRL2 `ltscompare` (its dylib closure staged under
`mcrl2/lib/` with `@loader_path/../lib` rpath, quarantine stripped) into a
`.tar.gz` in `dist/`. Packaging and publishing are **separate** — sign/notarize
the artifact if needed, then push it:

```bash
./scripts/package-macos.sh                     # build + package (into dist/)
# ...optionally codesign/notarize dist/nucleos-*.tar.gz...
./scripts/push-release-ftp.sh dist/nucleos-*.tar.gz   # upload
```

The package step prints the exact push command (with the FTP target dir) when
it finishes. [`scripts/push-release-ftp.sh`](./scripts/push-release-ftp.sh) is
OS-agnostic — it uploads any `dist/nucleos-*.{tar.gz,zip}` (Linux/Windows from
[`build-release.sh`](./scripts/build-release.sh) too).

**Before pushing**, create `scripts/ftp.env` with the download-server
credentials by copying the tracked template — this file is **gitignored**
(holds the real password), never commit it:

```sh
cp scripts/ftp.env.example scripts/ftp.env
chmod 600 scripts/ftp.env
$EDITOR scripts/ftp.env          # fill in FTP_IP / FTP_USER / FTP_PASS
```

The same values (`FTP_IP`/`FTP_USER`/`FTP_PASS`/`FTP_DIR`) can instead be
supplied as environment variables (e.g. in CI). Uploaded builds are served at
`https://downloads.verum.com/download/nucleos/`. Because the bundled
`ltscompare` is only ad-hoc signed, a browser-downloaded tarball is quarantined
— run `xattr -dr com.apple.quarantine <extracted-dir>` before first use (or
notarize). For the cross-platform release flow, see
[`RELEASING.md`](./RELEASING.md) and [`scripts/build-release.sh`](./scripts/build-release.sh).

## Dependencies

- **Rust** (2021 edition) — to build `nucleos`. This is the only dependency
  needed to build the binary.
- **mCRL2** (`ltscompare`, `ltsconvert`, `tracepp`) — *optional*, for LTS
  weak-failures equivalence checks: `nucleos verify`'s interface-compliance
  check and the `lts`/`verify`/`threads`/`lbs` comparisons in `nuctest`. It is
  **not** required to build or run the rest of `nucleos` — without it those
  comparisons degrade gracefully (`nucleos verify` prints
  `compliance checks require mCRL2 (ltscompare) on PATH; skipping` and runs all
  other checks; `nuctest` reports the affected models as skipped). To enable
  them, make `ltscompare` resolvable one of two ways:
  - put an `ltscompare` on your `PATH` (install mCRL2 — ideally **202407.1** to
    match Dezyne 2.20.0), or
  - run [`scripts/build-mcrl2.sh`](./scripts/build-mcrl2.sh) to build a
    version-matched, bundled `ltscompare` into `dist/mcrl2/<triple>/bin/`
    (needs `cmake` + `zig`; see the script header). Release archives ship this
    bundled copy automatically — this step is only for dev-from-source builds.

    `nucleos verify` looks for the bundled binary at `<exe-dir>/mcrl2/bin/`
    then falls back to `PATH`; `nuctest` looks at `dist/mcrl2/<triple>/bin/`
    then `PATH`.
- **dzn** (Dezyne CLI) — reference tool; required by the golden generators.

## Usage

```bash
# Parse / well-formedness
./target/release/nucleos parse model.dzn

# Simulate: replay a trace, from stdin or from a file
./target/release/nucleos simulate -m ComponentName -I imports/ model.dzn < trace.txt
./target/release/nucleos simulate -m ComponentName -I imports/ -t trace.txt model.dzn

# Simulate interactively: after each RTC nucleos prints the `(eligible …)`
# menu on stderr and reads the next event from stdin, one per line
./target/release/nucleos simulate --repl -m ComponentName -I imports/ model.dzn

# Verify
./target/release/nucleos verify -m ComponentName -I imports/ model.dzn

# LTS generation
./target/release/nucleos lts -m ComponentName -I imports/ model.dzn > out.aut
```

## Output directories

Most generated files land under `./build/` (gitignored). Paths are defined in
`config.sh` and every script sources it, so overriding is a single export away.
The two phenom paths are the exceptions — see the notes under the table.

| Var              | Default                           | What lives here                                             |
| ---------------- | --------------------------------- | ----------------------------------------------------------- |
| `BUILD_DIR`      | `./build`                         | root                                                        |
| `ARTIFACTS_DIR`  | `$BUILD_DIR/artifacts`            | semi-persistent goldens (LBS) and per-run scratch            |
| `OUTPUTS_DIR`    | `$BUILD_DIR/outputs`              | per-run LTS from `nucleos` (comparison scratch)             |
| `LOGS_DIR`       | `$BUILD_DIR/logs`                 | parallel-worker log aggregation                             |
| `GOLDENS_SUBDIR` | `.nuctest-goldens`                | name of the golden dir inside the phenom tree                |
| `PHENOM_COMPLIST`| `./phenom_components.txt`         | list of leaf phenom components                              |
| `PHENOM_GOLDEN`  | `$PHENOM/$GOLDENS_SUBDIR`         | per-component `.aut` + `.meta` goldens                      |

`PHENOM_COMPLIST` defaults to the **repo-root** list committed on this branch
(only PASS-clean components), not to a generated one under `build/`. Point it at
`$ARTIFACTS_DIR/phenom_components.txt` for the full corpus, or pass a path as
the first argument to `run_phenom_lts.sh`.

`PHENOM_GOLDEN` deliberately lives **next to the customer source**, under
`<PHENOM>/.nuctest-goldens/`, not in this repository — the goldens are customer
IP. It matches `PhenomConfig::goldens_dir` in `src/bin/nuctest/config.rs`, so the
scripts read exactly the files `nuctest --category phenom` compares against.

Override any of these inline, e.g.
`PHENOM_GOLDEN=/other/dir bash scripts/gen-phenom-goldens.sh`.

## Generating goldens

Goldens live next to the tests in `test-models/<name>/baseline/` (tracked in
git) or under `build/artifacts/` (regenerated per machine, not tracked).

### Per-model goldens (tracked, under `test-models/`)

```bash
# trace -> simulate.N golden for every (model, trace.N) pair (-> baseline/simulate.N)
bash gen_simulate_goldens.sh

# located-JSON goldens (dzn simulate -l | dzn trace -f json -> baseline/simulate-json.N)
bash gen_simulate_json_goldens.sh

# per-step (eligible ...) / (labels ...) goldens for simulate-repl (-> eligible.N.k / labels.N.k)
bash gen_eligible_goldens.sh
bash gen_labels_goldens.sh
```

Each writes a log under `build/logs/` and prints a one-line summary. Other
golden classes (verify, lts.aut, wfc, symres) were generated by dzn once and
are tracked; regenerate ad hoc with `dzn` only when a model changes
(see the per-category notes in `test-models/`).

### Phenom (industrial) goldens — under `<PHENOM>/.nuctest-goldens/`

```bash
# Discover leaf components -> $PHENOM_COMPLIST (repo root by default)
bash gen_phenom_components.sh

# Regenerate the per-component .aut + .meta goldens -> $PHENOM_GOLDEN
bash scripts/gen-phenom-goldens.sh
```

Requires a phenom source tree at `$PHENOM` (default `~/src/phenom`). Override
with `PHENOM=/path bash gen_phenom_components.sh`.

The goldens are customer IP and live beside that source tree, not in this
repository — which is also why `nuctest --category phenom` simply does not run
when no phenom tree is present.

## Running tests

The test runner is **nuctest** (`cargo build --release --bin nuctest`):

```bash
# everything (parsing, parse-compare, wfc, symres, lts, verify, lbs, phenom,
# threads, misc, simulate, simulate-repl, trace, simulate-json) — except the
# opt-in heavy categories (`selfcheck`), which must be named explicitly.
# `phenom` runs only when a phenom source tree is present.
./target/release/nuctest

# one category / a model subset / more workers
./target/release/nuctest --category simulate --filter 'ext_*' -j 16
```

`scripts/regression/check.sh` is the blocking regression gate for the render
categories (simulate / simulate-repl / trace / simulate-json) against the
committed PASS snapshots; `--update` re-baselines after blessing new passes.

### Ad-hoc / benchmark scripts (root)

| Script | Purpose |
| ------ | ------- |
| `bash run_simulate_tests.sh` | shell fallback for the simulate byte-compare (nuctest supersedes it). |
| `bash run_benchmark.sh` / `bash run_lbs_benchmark.sh` | timing benchmarks vs dzn goldens. |
| `bash run_phenom_lts.sh` / `bash run_phenom_threads.sh` | phenom LTS-diff / thread-scaling benchmarks. |
| `bash run_phenom_verify_dzn.sh` | reference `dzn verify` run (timing comparison). |
| `bash scripts/gen-phenom-verify-cache.sh` | cache reference `dzn verify` time+verdict per component — run **once**. |
| `[OUT=f] bash run_phenom_verify_compare.sh` | `nucleos verify` (live) vs cached `dzn verify`: speedup table. |

### Debug / inspection utilities

| Script | Purpose |
| ------ | ------- |
| `bash compare_lts.sh model.dzn golden.aut` | quick one-shot "ours vs golden" weak-trace compare. |
| `bash lts_compare.sh mine.aut golden.aut` | weak-failures refinement + queue-full path intersection. |
| `bash trace_lts.sh lts.aut evt1 evt2 ...` | walk a trace through an LTS, show visited states. |
| `bash check_handler_lts.sh` | generate Handler LTS, bisim-minimize, compare to golden, counter-example. |
| `bash categorize_fails.sh` | bucket failing LTS tests by blocking / external / fork / system. |
| `bash fix_imports.sh` | sync a few models from the dzn reference tree into this repo. |
| `bash scripts/phenom-verify-analysis.sh` | anonymize the corpus, correlate verify speedup vs. state-space size, emit an HTML plot. |

## Architecture

For the module layout, engine choice, and dispatch flow see
[`ARCHITECTURE.md`](./ARCHITECTURE.md). The short version:

- `src/lts/exec/` is the sole handler-body executor, emitting DAG-shape
  LTS subgraphs.
- `src/lts/bfs.rs` is the default engine: `generate_lts_parallel` runs
  `lts_explore_state` over a rayon pool with per-worker simulator clones.
- `src/lts/vector_bfs.rs` is an opt-in whole-state-vector BFS
  (`NUC_LPS2LTS=1`), not the default.

`ARCHITECTURE.md` is the authoritative description — prefer it to this
summary, which is necessarily lossy.

Dezyne language semantics are documented in
[`DEZYNE_SEMANTICS.md`](./DEZYNE_SEMANTICS.md); the changelog is
[`NEWS.md`](./NEWS.md).
