Command line

Install

On Linux or macOS:

curl -fsSL https://raw.githubusercontent.com/crowecawcaw/snappea/main/scripts/install.sh | sh

On Windows, in PowerShell:

irm https://raw.githubusercontent.com/crowecawcaw/snappea/main/scripts/install.ps1 | iex

The script downloads the latest GitHub release for your machine, checks it against the release's SHA256SUMS, and puts snappea in ~/.local/bin (Windows: %LOCALAPPDATA%\snappea\bin, added to your user PATH). It supports Linux x86_64 and arm64 with glibc, macOS on Intel and Apple silicon, and Windows x86_64.

To pin a version or pick the folder:

curl -fsSL https://raw.githubusercontent.com/crowecawcaw/snappea/main/scripts/install.sh | sh -s -- --version 0.1.0 --to /usr/local/bin

The same settings work as environment variables, SNAPPEA_VERSION and SNAPPEA_INSTALL_DIR, which is how the PowerShell script takes them. Check the install with snappea version.

Other ways to install

Quick start

The repository's example model is an inventory service with two designs for reserving stock. One is safe; the other lets two orders oversell:

git clone https://github.com/crowecawcaw/snappea
cd snappea/examples/model
snappea tests
snappea check tcAtomicReserve
snappea check tcCheckThenReserve

tests lists the two test cases. The safe design passes every possible ordering, and the other fails within a few schedules, with exit status 1:

Checking Inventory: 1 test case
ok    tcAtomicReserve (all 20277 schedules, 0.58s)
The test case passed in 0.58s, peak memory 6 MB. Output: PCheckerOutput/

Checking Inventory: 1 test case
FAIL  tcCheckThenReserve (bug found after 3 schedules, 4 workers, 0.00s)
      Assertion Failed: PSpec/inventory.p:27:7 reservation exceeds available stock
      Replay: snappea replay PCheckerOutput/tcCheckThenReserve/bug.schedule
1 of 1 test case failed in 0.00s, peak memory 6 MB. Output: PCheckerOutput/

PCheckerOutput/tcCheckThenReserve/bug.txt shows the two orders both reading 3 units of stock before either reserves.

You can also try models in the browser, with nothing installed, in the playground.

Sources

Commands that read P take .pproj or .p files as arguments. With none, they use the *.pproj file in the current folder, or else every *.p file in it and its immediate subfolders. So in a project folder, snappea check is usually enough. There is no separate compile step.

Exit status

This makes every command usable as a CI step or a pre-commit hook as it is.

Text and JSON

Every command prints text for people on a terminal or in CI, and a JSON result for agents and scripts otherwise. SNAPPEA_FORMAT=text or json sets the default; these options choose per run:

Output options work before or after the command. Unknown options and missing values also produce a JSON error result and write --json-report when requested. JSON keys retain insertion order.

snappea check

snappea check [SOURCE...] [TEST...] [options]

Checks test cases by exploring schedules: orderings of messages between machines, and the choices the model leaves open. A TEST is a test case name or a glob (tc*); with none, every test case is checked. It prints one line per test case with its coverage and, for a bug, the failing assertion and a snappea replay command. Then it lists the code no test case ran: handlers never triggered, if conditions never true or never false, and statements never reached.

Coverage from a test case stopped at its first bug is marked partial in the console and withcoverage.partial: true in JSON, including the combined total. Scenario coverage appears as a console summary and as scenarios artifacts in suite and test case JSON results. The coverage guide explains condition outcomes, transition pairs, and components excluded from the selected tests.

Search is automatic: small exhaustive searches can finish early; larger searches also try guided scheduling, deliberate actor delays, and priority scheduling. Competing sends and behavioral progress guide the allocation, while each scheduler keeps an exploration share. A timeout or coverage plateau does not establish that the model is correct. The default timeout is fixed at ten seconds per test.

When every test case passes, check then runs them against mutants: copies of the model with one small change, such as a removed statement, an if forced one way, or < swapped for <=. A change no test case detects is listed with its line: the code ran, but no spec or assertion depends on what it does. Add a spec, an assertion or a test case that would fail with the change, or suppress it with // snappea-lint: allow mutation[:kind] -- reason on the line before. Specs and test drivers are not mutated, and undetected mutants do not change the exit status. JSON results list them under mutation.undetected. Changes share the time limit round robin, so a run cut short gives each about the same number of schedules.

snappea check lint [SOURCE...] runs only the model lints, without exploring schedules. snappea check mutation [SOURCE...] [TEST...] runs only mutation testing, with a 5 minute limit by default, and exits with 1 when a change goes undetected, so CI can require every change to be detected or suppressed.

How much to explore

Mutation testing

Time and output

Output files

A test case that finds a bug writes to <DIR>/<TEST>/, replacing the previous run's files: bug.txt (the log of the failing schedule), bug.schedule and bug.trace.json. Scenario monitors also write scenario_coverage.json there.

snappea replay

snappea replay <FILE.schedule> [SOURCE...] [--test <NAME>] [-v]

Runs a schedule written by snappea check again, so you can fix the model or the design and confirm the bug is gone. Exit status 1 means the bug was reproduced. If the schedule was found with step options (--max-steps and the others), pass the same ones; the replay line that check prints includes them.

snappea tests

snappea tests [SOURCE...]

Type-checks the sources and lists their test cases, one per line. A fast first step in CI.

snappea observe

snappea observe [SOURCE...] [LOG...] --spec <NAME> [options]

Checks logs of a running system against P spec monitors. A LOG is a file, a folder of logs, or a quoted glob ("logs/**/*.jsonl"). By default each line is one JSON event. It prints one line per spec with its coverage (the spec's handlers, statements and branches the events ran), and lists the spec code no event ran. The observe guide covers log formats and live streams.

snappea coverage

snappea coverage merge [DIR]
snappea coverage merge-observe [RESULT.json ...] [--stdin]

merge combines the scenario coverage reports under a folder (for example, from several CI jobs) into one. merge-observe merges the coverage of snappea observe JSON results, without the P sources.