# 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** trace execution — interactive or from file (`nucleos <model>`)
- **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 assume this path — set
`BIN=...` before running a script to override.

`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 (interactive or trace-driven)
./target/release/nucleos -m ComponentName -I imports/ model.dzn
./target/release/nucleos -m ComponentName -I imports/ model.dzn < trace.txt

# 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

All generated files land under `./build/` (gitignored). Paths are defined in
`config.sh` and every script sources it, so overriding is a single export away.

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

Override any of these inline, e.g. `PHENOM_GOLDEN=/other/dir bash gen_phenom_golden.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
# dzn verify -v golden for every test-models/<name>/ (→ baseline/verify)
bash gen_verify_golden.sh

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

# dzn parse golden for wf_* rejection tests (→ <name>.wfc)
bash gen_wfc.sh [--dry-run]

# dzn parse golden for symres_* accept/reject tests (→ <name>.expect, <name>.wfc)
bash gen_symres.sh [--dry-run]
```

Each writes a log under `build/logs/` and prints a one-line summary.

### Ad-hoc LTS golden from dzn

```bash
# Produce a cleaned golden .aut via `dzn verify --out aut` (with graph fallback).
# Stderr carries DZN_MS=<wall-clock> for timing.
bash gen_golden.sh -m ComponentName -I imports/ model.dzn out.aut
```

Used internally by the LBS / phenom golden runners below.

### Phenom (industrial) goldens — under `build/artifacts/`

```bash
# 1. Discover leaf components → build/artifacts/phenom_components.txt
bash gen_phenom_components.sh

# 2. Run dzn on every leaf component → build/artifacts/phenom_golden/<comp>.{aut,meta}
bash gen_phenom_golden.sh
```

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

## Running tests

All runners default to `$(nproc)` workers — override with `JOBS=N bash …`.

### Unit regressions

| Script                         | What it checks                                                              |
| ------------------------------ | --------------------------------------------------------------------------- |
| `bash run_wf_tests.sh`         | well-formedness — nucleos rejects `wf_*` models with expected messages; plus false-positive scan on all other models (`--no-fp` to skip). |
| `bash run_symres_tests.sh`     | symbol-resolution accept/reject tests (`symres_*`), goldens from dzn.       |
| `bash run_verify_tests.sh`     | `nucleos verify -v` byte-equal to `baseline/verify`; LTS-vs-verify classifier on divergence. |
| `bash run_simulate_tests.sh`   | `nucleos <model> < trace.N` byte-equal to `baseline/simulate.N` (one task per trace). |
| `bash run_lts_tests.sh`        | serial LTS generator — weak-failures equivalence vs `baseline/lts.aut`.     |
| `bash run_lts_tests_parallel.sh` | parallel version of the above.                                            |
| `bash run_lts_tests_dpweak.sh` | dpweak-bisim / bisim comparison, consumes LTS already written to `build/outputs/lts_mine/`. |
| `bash run_handler_tests.sh`    | Handler model trace simulation (742 traces).                                |
| `bash run_external_tests.sh`   | external-port tests — weak-failures + queue-full path intersection.         |
| `bash run_regression.sh`       | generates LTS for every `lts/` model then runs LTS + WF + symres summaries. |

### LBS (LegoBallSorter) suite

Requires `$LBS` (default `~/src/dzn2.19/test/all/LegoBallSorter`).

| Script                          | Purpose                                                                |
| ------------------------------- | ---------------------------------------------------------------------- |
| `bash run_lbs_verify.sh`        | `nucleos verify` on behavior components; reports per-model time.       |
| `bash run_lbs_golden.sh`        | generate dzn goldens for leaf behavior components.                     |
| `bash run_lbs_components.sh`    | LTS compare (ours vs dzn golden) for every behavior component.         |
| `bash run_lbs_system_lts.sh`    | same, for system components, inner-to-outer.                           |
| `bash run_lbs_benchmark.sh`     | timing benchmark vs dzn golden.                                        |

### Phenom (industrial) suite

Needs the component list from `gen_phenom_components.sh` (and goldens from
`gen_phenom_golden.sh` for the LTS-diff scripts).

| Script                                | Purpose                                                                 |
| ------------------------------------- | ----------------------------------------------------------------------- |
| `bash run_phenom_verify.sh`           | `nucleos verify` per component, sequential.                             |
| `JOBS=N bash run_phenom_verify_parallel.sh` | parallel version.                                                  |
| `bash run_phenom_verify_dzn.sh`       | reference `dzn verify` run (for timing comparison).                     |
| `bash run_phenom_lts.sh`              | LTS-diff (ours vs golden) with weak-failures; prints states/time/speedup. |
| `bash run_phenom_threads.sh`          | scaling benchmark across thread counts.                                 |

### Benchmarks

| Script                     | Purpose                                                               |
| -------------------------- | --------------------------------------------------------------------- |
| `bash run_benchmark.sh`    | LTS + dzn-verify golden comparison across known-passing components.   |
| `bash run_lbs_benchmark.sh`| LBS-focused version of the above.                                     |

### 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.     |

### Git helpers

`bash git_commit.sh`, `bash git_init_commit.sh` — convenience wrappers used
for bootstrapping and routine commits.

## Test status

See individual runner output for current pass/fail counts. The script
runners (`run_lts_tests_parallel.sh`, `run_verify_tests.sh`,
`run_phenom_lts.sh`, etc.) print a one-line summary at the end.

## Architecture

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

- `step_frontier` (in `src/semantics/lts/step_frontier.rs`) is the
  canonical executor for single-component LTS and verify. Emits
  DAG-shape LTS subgraphs and is the default for everything.
- The legacy chain-shape engine (`exec.rs` + `explore.rs`) is retained
  for `is_system` / `is_interface` modes and for
  `ComponentLts::successors` (driven by `trace_render_multi` — the
  system composer needs chain-shape).
- `parallel.rs` runs `lts_explore_state` over a rayon thread pool with
  per-worker simulator clones.

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