Docs

Coming from P

The same language and the same results, with a different toolchain underneath.

Snap Pea is another implementation of the P toolchain, written in Rust. Your models, test cases and specs stay plain P, and checks produce the bug reports, traces and output folders you already know. Upstream P's language design, test suites, tutorials and golden traces are what Snap Pea is built and validated against, and they're the reason it can aim for exact compatibility at all.

The goal is to put P in more places: in CI on every change, inside application test suites in several languages, and in the browser.

At a glance

	P	Snap Pea
Checker	compiles models to C# and runs them on .NET	interprets the typed model directly
Workflow	`p compile`, then `p check`	`snappea check` reads `.pproj` or `.p` files
Command line	`p`	`snappea-compat` (same options and output), or `snappea`
Foreign code	C#, Java	Rust
Checking logs	PObserve, with compiled jars	`snappea observe`, with specs read from source
PVerifier	yes	not yet

Commands

snappea-compat is a drop-in replacement for p. Alias it and existing scripts keep working:

$ alias p=snappea-compat
$ p check -tc tcMyTest -s 1000          # no p compile first
$ p check -r PCheckerOutput/BugFinding/MyProject_0_0.schedule

snappea is the same checker with shorter options, concise output and one folder per test case. It finds the project the way p does:

$ snappea check tcMyTest                    # one test case, up to ten seconds
$ snappea check 'tcMy*' --timeout 5m           # a glob, five minutes each
$ snappea replay PCheckerOutput/tcMyTest/bug.schedule
$ snappea observe --spec BankBalanceCorrect logs/

What stays the same

These match upstream exactly in snappea-compat. snappea has its own options, console output and output folder (PCheckerOutput/<test>/bug.txt, bug.schedule, bug.trace.json, replaced by each run), resolves <IncludeProject> paths against the including project file first, and its observe writes no report folder.

check, merge-scenario-coverage and observe options, help, console output and exit codes.
Parse and type error messages; bug reports, assertion and liveness messages.
Trace files (.txt, .trace.json, .schedule), coverage reports, the output folder layout and history rotation.
.pproj files, and PObserve's output files.
With one worker (-j 1) and the same seed, the schedules upstream explores.

What differs

There's no compile step. check reads P sources, not a compiled .dll, and OutputDir and Target in .pproj files are ignored.
Foreign functions and log parsers are written in Rust, not C# or Java. snappea check rejects a project that lists .cs or .java files, since it cannot run them; pass --ignore-foreign-files to check the P model anyway. snappea-compat only warns.
snappea check runs one worker per CPU core by default. Each worker has its own seed, so a given --seed explores different schedules from upstream's, and which bug is reported can vary between runs.
Findings may be reported in a different order, and elapsed time and memory figures differ.
An action that loops forever without reaching a scheduling point is reported as a bug.
Not supported yet: PVerifier, PObserve's --filters, socket mode and SERIALIZEDEVENTS input. Out of scope: p compile output, and foreign code in C# or Java.

The compatibility reference has every detail.

What Snap Pea adds

Parallel workers: -j N splits the schedules across workers. The first bug stops them all, and its .schedule file replays as usual.
Exhaustive search: Exhaustive exploration runs automatically alongside sampled search, skipping states it has already seen. Completed exhaustive searches end early; searches that reach the timeout remain incomplete.
Time: --latency and --timed check timeouts and latency budgets with model time, using foreign functions and no new syntax. See the RetryBudget example.
Specs in application tests: Helpers for Python, Rust, Java and Go record events from ordinary tests and check them against your specs, with monitor coverage. See the integration examples.
More from observe: Several specs per run, --all-specs, --check-hot, --json-report, spec coverage, --strict and live input (--live). In snappea-compat observe, runs that use none of them behave as upstream. See snappea observe.
In the browser: The checker builds to WebAssembly, which runs the Playground with nothing to install.

How compatibility is tested

Upstream's own test suites are vendored in the repository and checked against:

All 424 compiler regression tests compile, or fail to, as upstream expects.
All 249 checker tests find a bug exactly when upstream expects one, across seeds.
The tutorials give the same results as upstream's tutorial CI.
Readable and JSON traces match upstream's golden files.
snappea-compat observe and PObserve are compared in CI on 96 vendored runs. 94 match after normalization; the remaining runs check only exit codes because of a null-dereference message difference. The separate manual comparison of the full upstream suite has 192 runs, with 186 outputs identical after normalization.

The upstream parity page has the measured corpus, normalization rules, known differences and reproduction commands. If Snap Pea disagrees with upstream on a model, that's a Snap Pea bug. Please report it. Validation and benchmarks have the details.

Learning P

Upstream's documentation, tutorials and case studies are the best way to learn the language, and every tutorial runs unchanged with snappea.