Snap Pea v0.1.0

What's Changed in v0.1.0

Features

• snappea check model-checks P models by interpreting the sources directly, with no compile step and no .NET. It reads the .pproj in the current folder, a .pproj or .p file given as an argument, or the local *.p files, and reports type errors in the same format as p compile. (#18)
• The snappea command line has check, replay, tests, observe and coverage merge-observe. Test cases can be given as arguments or globs, and options include -n, -j, --time with units (--time 5m), --strategy and --exhaustive. Exit status is 0 for no bug, 1 for a bug and 2 for an error. (#23)
• snappea check prints one line per test case. When a test case finds a bug, it also prints the bug report and the snappea replay command that reproduces it, then a summary with total time and peak memory. Upstream-style progress appears only with -v. Each test case's files go to <out>/<test>/ with fixed names (bug.txt, bug.schedule, bug.trace.json, coverage.txt, summary.txt, scenario_coverage.json). (#78)
• snappea replay prints the reproduced bug and accepts --max-steps, --fair-max-steps and --fail-on-max-steps, so bugs found with --fail-on-max-steps can be replayed. (#78)
• snappea-compat is a drop-in replacement for upstream's p tool. It accepts the same options and writes the same console output, text, JSON and XML traces, .schedule files, activity coverage reports and output folders. p compile is accepted and does nothing, so existing p compile && p check scripts still work. (#23, #18)
• The checker supports the random, pct, fairpct, probabilistic, pos, feedback, feedbackpct, feedbackpos and rl scheduling strategies, plus exhaustive search (snappea check --exhaustive, or --mode pex in snappea-compat), which skips states it has already visited and reports whether every behavior was explored. (#10)
• snappea check runs schedules on several worker threads, one per core by default (-j). Combined with a faster interpreter, checking the Raft tutorial is about 2.5× faster on one worker and about 8× faster with the default workers. -j 1 explores exactly the same schedules as upstream. (#21)
• P models can use scenario (coverage) monitors, with merge-scenario-coverage to combine their results, and foreign types and functions implemented in Rust. (c651c2a)
• Latency budgets: snappea check --latency FILE[:PROFILE] and --timed check models against message latencies. Specs checked with snappea observe can call Now(), NowBest(), Mark(), Elapsed() and ElapsedBest() to check latencies against log timestamps. (#26)
• snappea observe checks recorded event logs against P spec monitors, with no P model needed. Sources and logs are passed as arguments, globs are expanded, and the built-in parsers read JSON Lines and P traces. Custom parsers can be written in Rust. snappea-compat observe is a drop-in replacement for upstream PObserve and matches its console output, output files and exit codes. (#11, #58, #78)
• snappea observe options: --spec, --all-specs and --exclude-specs select several specs in one run; --json-report writes a machine-readable result; --check-hot reports keys left in a hot state; --strict fails when a selected spec saw no relevant events; and --unknown-events ignore|warn|error reports event names no P source declares, with a "did you mean" suggestion. (#25, #40, #56)
• snappea observe --coverage reports which monitor states, handlers and transitions the events exercised, as text and in the JSON report. snappea coverage merge-observe merges these reports across a test suite. (#34, #39, #55)
• snappea observe can check live inputs: --stdin and --live PATH (repeatable, including pipes and /dev/fd/N) stop at the first error without waiting for end of input. --sequence FIELD merges several live inputs by a sequence number, and --record FILE saves the checked lines. (#35, #58, #78)
• Python helper (pip install pysnappea, import snappea): code calls emit(...), and a pytest plugin checks each test's events against your P specs and fails the test if a spec is violated. It also provides check_spec, expect_violation, events from threads and child processes, monitor coverage across the suite, and a production sink with set_sink. The wheel includes the snappea binary. (#25, #36, #60, #63)
• Go helper (go get github.com/crowecawcaw/snappea): snappeatest records events during tests and checks them on cleanup, with typed *SpecViolation and *SetupError errors, ExpectViolation and suite coverage through snappeatest.Main. snappeaemit emits events and has a production sink. If the snappea binary isn't on PATH, the helper downloads the release binary and verifies its checksum. (#42, #61, #63, #66)
• Java helper (io.github.crowecawcaw:snappea) with no runtime dependencies: recordings, a JUnit 5 extension, expectViolation, structured SpecViolation and SetupError, suite coverage, and a production sink through SnappeaEmit. The native binary comes in a natives-<os>-<arch> jar. (#43, #59, #63, #67)
• Rust crate snappea: snappea::test checks events recorded during tests, using Model::load, expect_violation, structured SpecViolation and SetupError, and suite coverage. snappea::emit sends events, including to a production sink with set_sink. For production, build with default-features = false, features = ["emit"] to leave out the checker. (#41, #62, #63, #68)
• The browser playground edits, type-checks and model-checks P models with nothing sent to a server. It includes the upstream tutorials as demos and a step-through trace diagram linked to the log, and a machine filter shows only the steps of the machines you pick. (#4, #6, #51)
• Each GitHub release includes prebuilt snappea binaries for Linux (x86-64, ARM), macOS (Intel, Apple silicon) and Windows, with a SHA256SUMS file. cargo install snappea installs both snappea and snappea-compat. (#69)