Snap Pea

The P modeling language in Rust: a parser, type checker and model checker with no .NET, Java or code generation, plus helpers to check the events your application emits against P specs.

The snappea tool

cargo install snappea        # installs snappea and snappea-compat
snappea check                 # check every test case of the .pproj in this folder
snappea observe --spec BankBalanceCorrect logs/      # check production logs

snappea-compat is a drop-in replacement for upstream's p command.

Library

cargo add --dev snappea for tests. Production code needs only the emitter:

[dependencies]
snappea = { version = "0.1", default-features = false, features = ["emit"] }

[dev-dependencies]
snappea = "0.1"

// Application code. With only the `emit` feature, no checker is compiled in.
snappea::emit::emit("eReserved", "coffee", snappea::emit::json!({"order": "o1", "units": 2}));

// A test: everything emitted while the closure runs is checked against the P specs
// configured in [package.metadata.snappea] of Cargo.toml.
let model = snappea::test::Model::load()?;
model.check(|_recording| app.reserve("coffee", "o1", 2));

test and cli also expose the checker as a library: snappea::syntax, snappea::sema, snappea::checker, snappea::project and snappea::driver.

Documentation

• The repository: snappea usage and compatibility with upstream P
• Rust inventory examples
• Testing and production
• Checking logs with snappea observe
• The checker as a library

License

MIT or Apache-2.0, at your option.